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

Theorem syl9r 72
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
syl9r.1
syl9r.2
Assertion
Ref Expression
syl9r

Proof of Theorem syl9r
StepHypRef Expression
1 syl9r.1 . . 3
2 syl9r.2 . . 3
31, 2syl9 71 . 2
43com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  sylan9r  658  ax12v  1855  19.23t  1909  nfimd  1917  fununi  5659  dfimafn  5922  funimass3  6003  isomin  6233  oneqmin  6640  tz7.48lem  7125  fisupg  7788  trcl  8180  coflim  8662  coftr  8674  axdc3lem2  8852  konigthlem  8964  indpi  9306  nnsub  10599  2ndc1stc  19952  kgencn2  20058  tx1stc  20151  filuni  20386  fclscf  20526  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALT  20551  lpni  25181  dfimafnf  27473  dfon2lem6  29220  nodenselem8  29448  finixpnum  30038  heiborlem4  30310  dfaimafn  32250  imbi13  33290  lncvrelatN  35505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator