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

Theorem syl9r 72
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
syl9r.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl9r.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
syl9r  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )

Proof of Theorem syl9r
StepHypRef Expression
1 syl9r.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl9r.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9 71 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43com12 31 1  |-  ( th 
->  ( 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:  sylan9r  658  ax12v  1804  19.23t  1856  nfimd  1864  fununi  5653  dfimafn  5915  funimass3  5996  isomin  6220  oneqmin  6619  tz7.48lem  7106  fisupg  7767  trcl  8158  coflim  8640  coftr  8652  axdc3lem2  8830  konigthlem  8942  indpi  9284  nnsub  10573  2ndc1stc  19734  kgencn2  19809  tx1stc  19902  filuni  20137  fclscf  20277  alexsubALTlem2  20299  alexsubALTlem3  20300  alexsubALT  20302  lpni  24873  dfimafnf  27162  dfon2lem6  28813  nodenselem8  29041  finixpnum  29631  heiborlem4  29929  dfaimafn  31733  imbi13  32378  lncvrelatN  34586
  Copyright terms: Public domain W3C validator