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  656  ax12v  1860  19.23t  1914  nfimd  1922  fununi  5636  dfimafn  5897  funimass3  5979  isomin  6208  oneqmin  6613  tz7.48lem  7098  fisupg  7760  trcl  8150  coflim  8632  coftr  8644  axdc3lem2  8822  konigthlem  8934  indpi  9274  nnsub  10570  2ndc1stc  20118  kgencn2  20224  tx1stc  20317  filuni  20552  fclscf  20692  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALT  20717  lpni  25383  dfimafnf  27694  dfon2lem6  29460  nodenselem8  29688  finixpnum  30278  heiborlem4  30550  dfaimafn  32489  imbi13  33677  lncvrelatN  35902
  Copyright terms: Public domain W3C validator