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

Theorem syl9r 67
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 66 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43com12 27 1  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylan9r  639  oneqmin  4612  fununi  5332  dfimafn  5587  funimass3  5657  isomin  5850  tz7.48lem  6469  fisupg  7121  trcl  7426  coflim  7903  coftr  7915  axdc3lem2  8093  konigthlem  8206  indpi  8547  nnsub  9800  2ndc1stc  17193  kgencn2  17268  tx1stc  17360  filuni  17596  fclscf  17736  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALT  17761  lpni  20862  dfimafnf  23057  dfon2lem6  24215  nodenselem8  24413  limptlimpr2lem2  25678  heiborlem4  26641  dfaimafn  28133  imbi13  28582  lncvrelatN  30592
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator