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  6775  nnaordi  6847  fineqvlem  7309  dif1enOLD  7326  dif1en  7327  xpfi  7364  rankr1ag  7712  cfslb2n  8132  fin23lem27  8192  gchpwdom  8533  prlem934  8894  axpre-sup  9028  cju  9980  xrub  10874  facavg  11575  mulcn2  12372  o1rlimmul  12395  coprm  13083  rpexp  13103  vdwnnlem3  13348  gexdvds  15201  cnpnei  17311  alexsubALTlem3  18063  alexsubALTlem4  18064  iccntr  18835  cfil3i  19205  bcth3  19267  lgseisenlem2  21117  usgrasscusgra  21475  ubthlem1  22355  staddi  23732  stadd3i  23734  addltmulALT  23932  cnre2csqlem  24291  tpr2rico  24293  dfrdg4  25740  segconeq  25887  nn0prpwlem  26257  comppfsc  26319  fdc  26381  bfplem2  26464  frgrawopreglem4  28192  atexchcvrN  29968  dalem3  30192  cdleme3h  30763  cdleme21ct  30857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator