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  9078  nnncan  9082  nnncan2  9084  ltdivmul  9628  ledivmul  9629  ltdiv23  9647  lediv23  9648  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  dvdssub2  12566  dvdsgcdb  12723  vdwapun  13021  poslubdg  14252  ipodrsfi  14266  bddibl  19194  gxinv  20937  gxinv2  20938  vcnegsubdi2  21131  nvpi  21232  nvabs  21239  ghomgsg  24000  subdivcomb2  24091  lineid  24706  supdefa  25263  multinv  25422  islp3  25514  flfneih  25560  pell14qrgap  26960  sigarexp  27849  oplecon1b  29391  opltcon1b  29395  oldmm2  29408  oldmj2  29412  cmt3N  29441  2llnneN  29598  cvrexchlem  29608  pmod2iN  30038  polcon2N  30108  paddatclN  30138  osumcllem3N  30147  ltrnval1  30323  cdleme48fv  30688  cdlemg33b  30896  trlcolem  30915  cdlemh  31006  cdlemi1  31007  cdlemi2  31008  cdlemi  31009  cdlemk4  31023  cdlemk19u1  31158  cdlemn3  31387  hgmapfval  32079
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