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  7098  nnaordi  7170  fineqvlem  7641  dif1enOLD  7658  dif1en  7659  xpfi  7697  rankr1ag  8124  cfslb2n  8552  fin23lem27  8612  gchpwdom  8952  prlem934  9317  axpre-sup  9451  cju  10433  xrub  11389  facavg  12198  mulcn2  13195  o1rlimmul  13218  coprm  13908  rpexp  13928  vdwnnlem3  14180  gexdvds  16208  cnpnei  19010  alexsubALTlem3  19763  alexsubALTlem4  19764  iccntr  20540  cfil3i  20922  bcth3  20984  lgseisenlem2  22832  usgrasscusgra  23570  ubthlem1  24450  staddi  25829  stadd3i  25831  addltmulALT  26029  cnre2csqlem  26508  tpr2rico  26510  dfrdg4  28148  segconeq  28208  nn0prpwlem  28688  comppfsc  28750  fdc  28812  bfplem2  28893  usg2wlkeq  30460  nbhashuvtx1  30704  frgrawopreglem4  30811  bj-bary1lem1  32963  atexchcvrN  33447  dalem3  33671  cdleme3h  34242  cdleme21ct  34336
  Copyright terms: Public domain W3C validator