Theorem 2eximi 1581

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

Syntax hints:   -> wi 4   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excomim  1643  cgsex2g  2748  cgsex4g  2749  vtocl2  2767  vtocl3  2768  dtruarb  4152  opelopabsb  4220  mosubopt  4651  xpmlem  5006  brabvv  5867  ssoprab2i  5910  dmaddpqlem  7297  nqpi  7298  dmaddpq  7299  dmmulpq  7300  enq0sym  7352  enq0ref  7353  enq0tr  7354  nq0nn  7362  prarloc  7423  bj-inex  13493