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

Theorem 2eximi 1657
Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1
Assertion
Ref Expression
2eximi

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3
21eximi 1656 . 2
32eximi 1656 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  2mo  2373  2moOLD  2374  2eu6  2383  2eu6OLD  2384  cgsex2g  3143  cgsex4g  3144  vtocl2  3162  vtocl3  3163  dtru  4643  mosubopt  4750  elopaelxp  5077  xpdifid  5440  ssoprab2i  6391  hash1to3  12530  isfunc  15233  usgraop  24350  usgraedg4  24387  3v3e3cycl2  24664  frconngra  25021  ac6s6f  30581  2uasbanh  33334  2uasbanhVD  33711  bnj605  33965  bnj607  33974  bnj916  33991  bnj996  34013  bnj907  34023  bnj1128  34046  bj-dtru  34383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator