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

Theorem syl9 71
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 67 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  72  com23  78  sylan9  657  19.21t  1838  axc9lem1  1945  axc9lem2  1988  axc11n  1997  sbequi  2066  sbal1OLD  2172  reuss2  3635  reupick  3639  ordtr2  4768  suc11  4827  elres  5150  funimass4  5747  fliftfun  6010  omlimcl  7022  nneob  7096  rankwflemb  8005  cflm  8424  domtriomlem  8616  grothomex  9001  sup3  10292  caubnd  12851  fbflim2  19555  ellimc3  21359  dfon2lem6  27606  opnrebl2  28521  pm11.71  29655  axc11next  29665  3cyclfrgrarn1  30609  bj-axc11nv  32256  stdpc5t  32340  diaintclN  34708  dibintclN  34817  dihintcl  34994
  Copyright terms: Public domain W3C validator