MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an2 Unicode version

Theorem syld3an2 1229
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an2.1  |-  ( (
ph  /\  ch  /\  th )  ->  ps )
syld3an2.2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
Assertion
Ref Expression
syld3an2  |-  ( (
ph  /\  ch  /\  th )  ->  ta )

Proof of Theorem syld3an2
StepHypRef Expression
1 syld3an2.1 . . . 4  |-  ( (
ph  /\  ch  /\  th )  ->  ps )
213com23 1157 . . 3  |-  ( (
ph  /\  th  /\  ch )  ->  ps )
3 syld3an2.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com23 1157 . . 3  |-  ( (
ph  /\  th  /\  ps )  ->  ta )
52, 4syld3an3 1227 . 2  |-  ( (
ph  /\  th  /\  ch )  ->  ta )
653com23 1157 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  nppcan2  9094  nnncan  9098  nnncan2  9100  ltdivmul  9644  ledivmul  9645  ltdiv23  9663  lediv23  9664  xrmaxlt  10526  xrltmin  10527  xrmaxle  10528  xrlemin  10529  dvdssub2  12582  dvdsgcdb  12739  vdwapun  13037  poslubdg  14268  ipodrsfi  14282  bddibl  19210  gxinv  20953  gxinv2  20954  vcnegsubdi2  21147  nvpi  21248  nvabs  21255  ghomgsg  24015  subdivcomb2  24106  lineid  24778  supdefa  25366  multinv  25525  islp3  25617  flfneih  25663  pell14qrgap  27063  sigarexp  27952  oplecon1b  30013  opltcon1b  30017  oldmm2  30030  oldmj2  30034  cmt3N  30063  2llnneN  30220  cvrexchlem  30230  pmod2iN  30660  polcon2N  30730  paddatclN  30760  osumcllem3N  30769  ltrnval1  30945  cdleme48fv  31310  cdlemg33b  31518  trlcolem  31537  cdlemh  31628  cdlemi1  31629  cdlemi2  31630  cdlemi  31631  cdlemk4  31645  cdlemk19u1  31780  cdlemn3  32009  hgmapfval  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator