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  6544  nnaordi  6616  fineqvlem  7077  dif1enOLD  7090  dif1en  7091  xpfi  7128  rankr1ag  7474  cfslb2n  7894  fin23lem27  7954  gchpwdom  8296  prlem934  8657  axpre-sup  8791  cju  9742  xrub  10630  facavg  11314  mulcn2  12069  o1rlimmul  12092  coprm  12779  rpexp  12799  vdwnnlem3  13044  gexdvds  14895  cnpnei  16993  alexsubALTlem3  17743  alexsubALTlem4  17744  iccntr  18326  cfil3i  18695  bcth3  18753  lgseisenlem2  20589  ubthlem1  21449  staddi  22826  stadd3i  22828  addltmulALT  23026  tpr2rico  23296  dfrdg4  24488  segconeq  24633  copsexgb  24966  cmpmon  25815  nn0prpwlem  26238  comppfsc  26307  fdc  26455  bfplem2  26547  atexchcvrN  29629  dalem3  29853  cdleme3h  30424  cdleme21ct  30518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator