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

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
StepHypRef Expression
1 sylan9r.1 . . 3
2 sylan9r.2 . . 3
31, 2syl9r 72 . 2
43imp 429 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator