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

Theorem sylan9r 640
 Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-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 69 . 2
43imp 419 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359 This theorem is referenced by:  spimt  1953  sbequi  2106  limsssuc  4784  tfindsg  4794  findsg  4826  f1oweALT  6027  oaordi  6739  pssnn  7277  inf3lem2  7531  cardlim  7806  ac10ct  7862  cardaleph  7917  cfub  8076  cfcoflem  8099  hsmexlem2  8254  zorn2lem7  8329  pwcfsdom  8405  grur1a  8641  genpcd  8830  supmul  9922  zeo  10301  uzwo  10485  uzwoOLD  10486  xrub  10836  iccsupr  10943  climuni  12287  efgi2  15298  opnnei  17125  tgcn  17256  uffix  17892  alexsubALTlem2  18018  alexsubALT  18021  metrest  18493  causs  19190  subgoablo  21819  ocin  22718  spanuni  22966  superpos  23777  3orel13  25096  trpredmintr  25417  frmin  25425  nndivsub  26080  supadd  26107  locfincf  26238  cover2  26267  metf1o  26313  stoweidlem62  27640  bnj518  28903  sbequiNEW7  29222 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361
 Copyright terms: Public domain W3C validator