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

Step	Hyp	Ref	Expression
1		eximi.1	. . 3
2	1	eximi 1656	. 2
3	2	eximi 1656	1

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