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

Theorem syl9 69
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-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 65 1  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl9r  70  com23  75  sylan9  640  19.21t  1814  19.21tOLD  1887  ax12olem2  2007  ax10  2026  sbequi  2112  sbequiOLD  2116  sbal1  2205  reuss2  3623  reupick  3627  ordtr2  4627  suc11  4687  elres  5183  funimass4  5779  fliftfun  6036  tfrlem1  6638  omlimcl  6823  nneob  6897  rankwflemb  7721  cflm  8132  domtriomlem  8324  grothomex  8706  sup3  9967  caubnd  12164  spwmo  14660  fbflim2  18011  ellimc3  19768  dfon2lem6  25417  opnrebl2  26326  pm11.71  27575  ax10ext  27585  cshwssizelem1a  28281  3cyclfrgrarn1  28404  sbequiNEW7  29581  sbal1NEW7  29617  diaintclN  31858  dibintclN  31967  dihintcl  32144
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator