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  6718  nnaordi  6790  fineqvlem  7252  dif1enOLD  7269  dif1en  7270  xpfi  7307  rankr1ag  7654  cfslb2n  8074  fin23lem27  8134  gchpwdom  8475  prlem934  8836  axpre-sup  8970  cju  9921  xrub  10815  facavg  11512  mulcn2  12309  o1rlimmul  12332  coprm  13020  rpexp  13040  vdwnnlem3  13285  gexdvds  15138  cnpnei  17243  alexsubALTlem3  17994  alexsubALTlem4  17995  iccntr  18716  cfil3i  19086  bcth3  19146  lgseisenlem2  20994  usgrasscusgra  21351  ubthlem1  22213  staddi  23590  stadd3i  23592  addltmulALT  23790  cnre2csqlem  24105  tpr2rico  24107  dfrdg4  25506  segconeq  25651  nn0prpwlem  26009  comppfsc  26071  fdc  26133  bfplem2  26216  frgrawopreglem4  27792  atexchcvrN  29605  dalem3  29829  cdleme3h  30400  cdleme21ct  30494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator