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

Theorem 3syld 55
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 44 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 44 1  |-  ( ph  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  oaordi  6973  nnaordi  7045  fineqvlem  7515  dif1enOLD  7532  dif1en  7533  xpfi  7571  rankr1ag  7997  cfslb2n  8425  fin23lem27  8485  gchpwdom  8825  prlem934  9190  axpre-sup  9324  cju  10306  xrub  11262  facavg  12061  mulcn2  13057  o1rlimmul  13080  coprm  13769  rpexp  13789  vdwnnlem3  14041  gexdvds  16063  cnpnei  18710  alexsubALTlem3  19463  alexsubALTlem4  19464  iccntr  20240  cfil3i  20622  bcth3  20684  lgseisenlem2  22574  usgrasscusgra  23214  ubthlem1  24094  staddi  25473  stadd3i  25475  addltmulALT  25673  cnre2csqlem  26194  tpr2rico  26196  dfrdg4  27828  segconeq  27888  nn0prpwlem  28361  comppfsc  28423  fdc  28485  bfplem2  28566  usg2wlkeq  30135  nbhashuvtx1  30379  frgrawopreglem4  30486  bj-bary1lem1  32196  atexchcvrN  32678  dalem3  32902  cdleme3h  33473  cdleme21ct  33567
  Copyright terms: Public domain W3C validator