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

Theorem 3syld 51
Description: Triple syllogism deduction. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypotheses
Ref Expression
3syld.1  |-  ( ph  ->  ( ps  ->  ch ) )
3syld.2  |-  ( ph  ->  ( ch  ->  th )
)
3syld.3  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
3syld  |-  ( ph  ->  ( ps  ->  ta ) )

Proof of Theorem 3syld
StepHypRef Expression
1 3syld.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 3syld.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
31, 2syld 40 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 40 1  |-  ( ph  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  oaordi  6586  nnaordi  6658  fineqvlem  7120  dif1enOLD  7135  dif1en  7136  xpfi  7173  rankr1ag  7519  cfslb2n  7939  fin23lem27  7999  gchpwdom  8341  prlem934  8702  axpre-sup  8836  cju  9787  xrub  10677  facavg  11361  mulcn2  12116  o1rlimmul  12139  coprm  12826  rpexp  12846  vdwnnlem3  13091  gexdvds  14944  cnpnei  17049  alexsubALTlem3  17795  alexsubALTlem4  17796  iccntr  18378  cfil3i  18748  bcth3  18806  lgseisenlem2  20642  ubthlem1  21504  staddi  22881  stadd3i  22883  addltmulALT  23081  tpr2rico  23379  dfrdg4  24874  segconeq  25019  nn0prpwlem  25387  comppfsc  25456  fdc  25604  bfplem2  25695  atexchcvrN  29447  dalem3  29671  cdleme3h  30242  cdleme21ct  30336
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator