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

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