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

Theorem syl9r 73
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 72 . 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  670  ax12v2  1952  ax12vOLD  1953  ax12vOLDOLD  1954  19.23tOLD  2012  nfimd  2020  fununi  5659  dfimafn  5928  funimass3  6013  isomin  6246  oneqmin  6651  tz7.48lem  7176  fisupg  7837  fiinfg  8033  trcl  8230  coflim  8709  coftr  8721  axdc3lem2  8899  konigthlem  9011  indpi  9350  nnsub  10670  2ndc1stc  20543  kgencn2  20649  tx1stc  20742  filuni  20978  fclscf  21118  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALT  21144  lpni  25990  dfimafnf  28309  dfon2lem6  30505  nodenselem8  30648  finixpnum  31994  heiborlem4  32210  lncvrelatN  33417  imbi13  36947  dfaimafn  38812
  Copyright terms: Public domain W3C validator