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  19.23t  1842  nfimd  1850  fununi  5484  dfimafn  5740  funimass3  5819  isomin  6028  oneqmin  6416  tz7.48lem  6896  fisupg  7560  trcl  7948  coflim  8430  coftr  8442  axdc3lem2  8620  konigthlem  8732  indpi  9076  nnsub  10360  2ndc1stc  19055  kgencn2  19130  tx1stc  19223  filuni  19458  fclscf  19598  alexsubALTlem2  19620  alexsubALTlem3  19621  alexsubALT  19623  lpni  23666  dfimafnf  25950  dfon2lem6  27601  nodenselem8  27829  finixpnum  28414  heiborlem4  28713  dfaimafn  30071  imbi13  31225  lncvrelatN  33425
  Copyright terms: Public domain W3C validator