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

Theorem 3syld 54
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 43 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 43 1  |-  ( ph  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  oaordi  6791  nnaordi  6863  fineqvlem  7325  dif1enOLD  7342  dif1en  7343  xpfi  7380  rankr1ag  7730  cfslb2n  8150  fin23lem27  8210  gchpwdom  8551  prlem934  8912  axpre-sup  9046  cju  9998  xrub  10892  facavg  11594  mulcn2  12391  o1rlimmul  12414  coprm  13102  rpexp  13122  vdwnnlem3  13367  gexdvds  15220  cnpnei  17330  alexsubALTlem3  18082  alexsubALTlem4  18083  iccntr  18854  cfil3i  19224  bcth3  19286  lgseisenlem2  21136  usgrasscusgra  21494  ubthlem1  22374  staddi  23751  stadd3i  23753  addltmulALT  23951  cnre2csqlem  24310  tpr2rico  24312  dfrdg4  25797  segconeq  25946  nn0prpwlem  26327  comppfsc  26389  fdc  26451  bfplem2  26534  usg2wlkeq  28330  nbhashuvtx1  28419  frgrawopreglem4  28498  atexchcvrN  30299  dalem3  30523  cdleme3h  31094  cdleme21ct  31188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator