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  4328  opelopabsb  4402  mosubopt  4840  xpmlem  5208  brabvv  6134  ssoprab2i  6177  dmaddpqlem  7744  nqpi  7745  dmaddpq  7746  dmmulpq  7747  enq0sym  7799  enq0ref  7800  enq0tr  7801  nq0nn  7809  prarloc  7870  bj-inex  16933