Theorem 2eximi 1654

Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
eximi.1	|- ( ph -> ps )

Assertion

Ref	Expression
2eximi	|- ( E. x E. y ph -> E. x E. y ps )

Proof of Theorem 2eximi

Step	Hyp	Ref	Expression
1		eximi.1	. . 3 |- ( ph -> ps )
2	1	eximi 1653	. 2 |- ( E. y ph -> E. y ps )
3	2	eximi 1653	1 |- ( E. x E. y ph -> E. x E. y ps )

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  excomim  1715  cgsex2g  2858  cgsex4g  2859  vtocl2  2878  vtocl3  2879  dtruarb  4330  opelopabsb  4404  mosubopt  4842  xpmlem  5211  brabvv  6137  ssoprab2i  6180  dmaddpqlem  7750  nqpi  7751  dmaddpq  7752  dmmulpq  7753  enq0sym  7805  enq0ref  7806  enq0tr  7807  nq0nn  7815  prarloc  7876  bj-inex  17138