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

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3
2		syl9r.2	. . 3
3	1, 2	syl9 71	. 2
4	3	com12 31	1

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