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

Theorem 3syld 54
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 43 . 2  |-  ( ph  ->  ( ps  ->  th )
)
4 3syld.3 . 2  |-  ( ph  ->  ( th  ->  ta ) )
53, 4syld 43 1  |-  ( ph  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  oaordi  6825  nnaordi  6897  fineqvlem  7359  dif1enOLD  7376  dif1en  7377  xpfi  7414  rankr1ag  7764  cfslb2n  8186  fin23lem27  8246  gchpwdom  8583  prlem934  8948  axpre-sup  9082  cju  10034  xrub  10928  facavg  11630  mulcn2  12427  o1rlimmul  12450  coprm  13138  rpexp  13158  vdwnnlem3  13403  gexdvds  15256  cnpnei  17366  alexsubALTlem3  18118  alexsubALTlem4  18119  iccntr  18890  cfil3i  19260  bcth3  19322  lgseisenlem2  21172  usgrasscusgra  21530  ubthlem1  22410  staddi  23787  stadd3i  23789  addltmulALT  23987  cnre2csqlem  24343  tpr2rico  24345  dfrdg4  25830  segconeq  25979  nn0prpwlem  26367  comppfsc  26429  fdc  26491  bfplem2  26574  usg2wlkeq  28440  nbhashuvtx1  28529  frgrawopreglem4  28608  atexchcvrN  30411  dalem3  30635  cdleme3h  31206  cdleme21ct  31300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator