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  7207  nnaordi  7279  fineqvlem  7746  dif1enOLD  7764  dif1en  7765  xpfi  7803  rankr1ag  8232  cfslb2n  8660  fin23lem27  8720  gchpwdom  9060  prlem934  9423  axpre-sup  9558  cju  10544  xrub  11515  facavg  12359  mulcn2  13398  o1rlimmul  13421  coprm  14117  rpexp  14137  vdwnnlem3  14391  gexdvds  16477  cnpnei  19633  comppfsc  19901  alexsubALTlem3  20417  alexsubALTlem4  20418  iccntr  21194  cfil3i  21576  bcth3  21638  lgseisenlem2  23491  usgrasscusgra  24306  usg2wlkeq  24531  nbhashuvtx1  24738  frgrawopreglem4  24871  ubthlem1  25609  staddi  26988  stadd3i  26990  addltmulALT  27188  cnre2csqlem  27717  tpr2rico  27719  dfrdg4  29527  segconeq  29587  nn0prpwlem  30067  fdc  30165  bfplem2  30246  bj-bary1lem1  34153  atexchcvrN  34637  dalem3  34861  cdleme3h  35432  cdleme21ct  35526
  Copyright terms: Public domain W3C validator