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  4596  fununi  5316  dfimafn  5571  funimass3  5641  isomin  5834  tz7.48lem  6453  fisupg  7105  trcl  7410  coflim  7887  coftr  7899  axdc3lem2  8077  konigthlem  8190  indpi  8531  nnsub  9784  2ndc1stc  17177  kgencn2  17252  tx1stc  17344  filuni  17580  fclscf  17720  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALT  17745  lpni  20846  dfimafnf  23041  dfon2lem6  24144  nodenselem8  24342  limptlimpr2lem2  25575  heiborlem4  26538  dfaimafn  28027  imbi13  28283  lncvrelatN  29970
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator