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

Theorem syl9r 69
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-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 68 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43com12 29 1  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylan9r  640  19.23t  1808  nfimd  1817  oneqmin  4725  fununi  5457  dfimafn  5714  funimass3  5785  isomin  5996  tz7.48lem  6634  fisupg  7291  trcl  7597  coflim  8074  coftr  8086  axdc3lem2  8264  konigthlem  8376  indpi  8717  nnsub  9970  2ndc1stc  17435  kgencn2  17510  tx1stc  17603  filuni  17838  fclscf  17978  alexsubALTlem2  18000  alexsubALTlem3  18001  alexsubALT  18003  lpni  21615  dfimafnf  23886  dfon2lem6  25168  nodenselem8  25366  heiborlem4  26214  dfaimafn  27698  imbi13  27947  lncvrelatN  29895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator