MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl9r Structured version   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  1818  nfimd  1827  oneqmin  4777  fununi  5509  dfimafn  5767  funimass3  5838  isomin  6049  tz7.48lem  6690  fisupg  7347  trcl  7656  coflim  8133  coftr  8145  axdc3lem2  8323  konigthlem  8435  indpi  8776  nnsub  10030  2ndc1stc  17506  kgencn2  17581  tx1stc  17674  filuni  17909  fclscf  18049  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALT  18074  lpni  21759  dfimafnf  24035  dfon2lem6  25407  nodenselem8  25635  heiborlem4  26514  dfaimafn  27996  imbi13  28541  lncvrelatN  30515
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator