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

Theorem 3syld 53
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 42 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 42 1  |-  ( ph  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  oaordi  6748  nnaordi  6820  fineqvlem  7282  dif1enOLD  7299  dif1en  7300  xpfi  7337  rankr1ag  7684  cfslb2n  8104  fin23lem27  8164  gchpwdom  8505  prlem934  8866  axpre-sup  9000  cju  9952  xrub  10846  facavg  11547  mulcn2  12344  o1rlimmul  12367  coprm  13055  rpexp  13075  vdwnnlem3  13320  gexdvds  15173  cnpnei  17282  alexsubALTlem3  18033  alexsubALTlem4  18034  iccntr  18805  cfil3i  19175  bcth3  19237  lgseisenlem2  21087  usgrasscusgra  21445  ubthlem1  22325  staddi  23702  stadd3i  23704  addltmulALT  23902  cnre2csqlem  24261  tpr2rico  24263  dfrdg4  25703  segconeq  25848  nn0prpwlem  26215  comppfsc  26277  fdc  26339  bfplem2  26422  frgrawopreglem4  28150  atexchcvrN  29922  dalem3  30146  cdleme3h  30717  cdleme21ct  30811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator