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

Theorem 3syld 57
Description: Triple syllogism deduction. Deduction associated with 3syld 57. (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 45 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 45 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  7251  nnaordi  7323  fineqvlem  7788  dif1en  7806  xpfi  7844  rankr1ag  8274  cfslb2n  8698  fin23lem27  8758  gchpwdom  9095  prlem934  9458  axpre-sup  9593  cju  10605  xrub  11597  facavg  12485  mulcn2  13646  o1rlimmul  13669  coprm  14644  rpexp  14659  vdwnnlem3  14934  gexdvds  17222  cnpnei  20266  comppfsc  20533  alexsubALTlem3  21050  alexsubALTlem4  21051  iccntr  21825  cfil3i  22225  bcth3  22285  lgseisenlem2  24264  usgrasscusgra  25196  usg2wlkeq  25421  nbhashuvtx1  25628  frgrawopreglem4  25760  ubthlem1  26497  staddi  27884  stadd3i  27886  addltmulALT  28084  cnre2csqlem  28711  tpr2rico  28713  mclsax  30202  dfrdg4  30710  segconeq  30769  nn0prpwlem  30970  bj-bary1lem1  31667  poimirlem29  31882  fdc  31987  bfplem2  32068  atexchcvrN  32923  dalem3  33147  cdleme3h  33719  cdleme21ct  33814  bgoldbwt  38589  bgoldbst  38590  nnsum4primesodd  38602  nnsum4primesoddALTV  38603  dignn0flhalflem1  39699
  Copyright terms: Public domain W3C validator