Theorem sylan9 657

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1
sylan9.2

Assertion

Ref	Expression
sylan9

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3
2		sylan9.2	. . 3
3	1, 2	syl9 71	. 2
4	3	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  rspc2  3218  rspc3v  3222  trintss  4561  copsexg  4737  copsexgOLD  4738  chfnrn  5998  fvcofneq  6039  ffnfv  6057  f1elima  6171  onint  6630  peano5  6723  f1oweALT  6784  smoel2  7053  pssnn  7758  fiint  7817  dffi2  7903  alephnbtwn  8473  cfcof  8675  zorn2lem7  8903  suplem1pr  9451  addsrpr  9473  mulsrpr  9474  cau3lem  13187  divalglem8  14058  efgi  16737  elfrlmbasn0  18796  locfincmp  20027  tx1stc  20151  fbunfip  20370  filuni  20386  ufileu  20420  rescncf  21401  shmodsi  26307  spanuni  26462  spansneleq  26488  mdi  27214  dmdi  27221  dmdi4  27226  funimass4f  27474  ffnafv  32256  bj-ax89  34238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371