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

Theorem syld3an2 1231
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 1159 . . 3  |-  ( (
ph  /\  th  /\  ch )  ->  ps )
3 syld3an2.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com23 1159 . . 3  |-  ( (
ph  /\  th  /\  ps )  ->  ta )
52, 4syld3an3 1229 . 2  |-  ( (
ph  /\  th  /\  ch )  ->  ta )
653com23 1159 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  nppcan2  9288  nnncan  9292  nnncan2  9294  ltdivmul  9838  ledivmul  9839  ltdiv23  9857  lediv23  9858  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  dvdssub2  12842  dvdsgcdb  12999  vdwapun  13297  poslubdg  14530  ipodrsfi  14544  bddibl  19684  gxinv  21811  gxinv2  21812  vcnegsubdi2  22007  nvpi  22108  nvabs  22115  nmmulg  24305  ghomgsg  25057  subdivcomb2  25149  lineid  25921  pell14qrgap  26828  stoweidlem22  27638  stoweidlem26  27642  sigarexp  27716  oplecon1b  29684  opltcon1b  29688  oldmm2  29701  oldmj2  29705  cmt3N  29734  2llnneN  29891  cvrexchlem  29901  pmod2iN  30331  polcon2N  30401  paddatclN  30431  osumcllem3N  30440  ltrnval1  30616  cdleme48fv  30981  cdlemg33b  31189  trlcolem  31208  cdlemh  31299  cdlemi1  31300  cdlemi2  31301  cdlemi  31302  cdlemk4  31316  cdlemk19u1  31451  cdlemn3  31680  hgmapfval  32372
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator