Theorem 2eximi 1612

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

Syntax hints:   -> wi 4   E.wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1674  cgsex2g  2796  cgsex4g  2797  vtocl2  2815  vtocl3  2816  dtruarb  4220  opelopabsb  4290  mosubopt  4724  xpmlem  5086  brabvv  5964  ssoprab2i  6007  dmaddpqlem  7437  nqpi  7438  dmaddpq  7439  dmmulpq  7440  enq0sym  7492  enq0ref  7493  enq0tr  7494  nq0nn  7502  prarloc  7563  bj-inex  15399