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

Theorem syl9 73
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl9.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
syl9  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
32a1i 11 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ta ) ) )
41, 3syl5d 69 1  |-  ( ph  ->  ( th  ->  ( 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:  syl9r  74  com23  81  sylan9  662  19.21t  1985  axc9lem1  2092  axc9lem2  2132  axc9lem2OLD  2133  axc11n  2142  axc11nALT  2143  sbequi  2203  reuss2  3722  reupick  3726  elres  5139  ordtr2  5466  suc11  5525  funimass4  5914  fliftfun  6203  omlimcl  7276  nneob  7350  rankwflemb  8261  cflm  8677  domtriomlem  8869  grothomex  9251  sup3  10563  caubnd  13414  fbflim2  20985  ellimc3  22827  3cyclfrgrarn1  25733  dfon2lem6  30427  opnrebl2  30970  bj-axc11nv  31341  stdpc5t  31422  diaintclN  34620  dibintclN  34729  dihintcl  34906  pm11.71  36741  axc11next  36751  usgruspgrb  39254  usgredgsscusgredg  39503
  Copyright terms: Public domain W3C validator