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  6560  nnaordi  6632  fineqvlem  7093  dif1enOLD  7106  dif1en  7107  xpfi  7144  rankr1ag  7490  cfslb2n  7910  fin23lem27  7970  gchpwdom  8312  prlem934  8673  axpre-sup  8807  cju  9758  xrub  10646  facavg  11330  mulcn2  12085  o1rlimmul  12108  coprm  12795  rpexp  12815  vdwnnlem3  13060  gexdvds  14911  cnpnei  17009  alexsubALTlem3  17759  alexsubALTlem4  17760  iccntr  18342  cfil3i  18711  bcth3  18769  lgseisenlem2  20605  ubthlem1  21465  staddi  22842  stadd3i  22844  addltmulALT  23042  tpr2rico  23311  dfrdg4  24560  segconeq  24705  copsexgb  25069  cmpmon  25918  nn0prpwlem  26341  comppfsc  26410  fdc  26558  bfplem2  26650  atexchcvrN  30251  dalem3  30475  cdleme3h  31046  cdleme21ct  31140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator