Theorem sylan9r 658

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

Ref	Expression
sylan9r.1
sylan9r.2

Assertion

Ref	Expression
sylan9r

Proof of Theorem sylan9r

Step	Hyp	Ref	Expression
1		sylan9r.1	. . 3
2		sylan9r.2	. . 3
3	1, 2	syl9r 72	. 2
4	3	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  spimt  2005  limsssuc  6685  tfindsg  6695  findsg  6727  f1oweALT  6784  oaordi  7214  pssnn  7758  inf3lem2  8067  cardlim  8374  ac10ct  8436  cardaleph  8491  cfub  8650  cfcoflem  8673  hsmexlem2  8828  zorn2lem7  8903  pwcfsdom  8979  grur1a  9218  genpcd  9405  supmul  10536  zeo  10973  uzwo  11173  uzwoOLD  11174  xrub  11532  iccsupr  11646  reuccats1lem  12705  climuni  13375  efgi2  16743  opnnei  19621  tgcn  19753  locfincf  20032  uffix  20422  alexsubALTlem2  20548  alexsubALT  20551  metrest  21027  causs  21737  subgoablo  25313  ocin  26214  spanuni  26462  superpos  27273  3orel13  29094  trpredmintr  29314  frmin  29322  nndivsub  29922  supadd  30042  cover2  30204  metf1o  30248  stoweidlem62  31844  bnj518  33944  bj-spimtv  34278

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