Theorem 2eximi 1601

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 1600	. 2 |- ( E. y ph -> E. y ps )
3	2	eximi 1600	1 |- ( E. x E. y ph -> E. x E. y ps )

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1663  cgsex2g  2773  cgsex4g  2774  vtocl2  2792  vtocl3  2793  dtruarb  4189  opelopabsb  4258  mosubopt  4689  xpmlem  5046  brabvv  5916  ssoprab2i  5959  dmaddpqlem  7371  nqpi  7372  dmaddpq  7373  dmmulpq  7374  enq0sym  7426  enq0ref  7427  enq0tr  7428  nq0nn  7436  prarloc  7497  bj-inex  14430