Theorem 2eximi 1649

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

Syntax hints:   -> wi 4   E.wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1711  cgsex2g  2839  cgsex4g  2840  vtocl2  2859  vtocl3  2860  dtruarb  4281  opelopabsb  4354  mosubopt  4791  xpmlem  5157  brabvv  6066  ssoprab2i  6109  dmaddpqlem  7596  nqpi  7597  dmaddpq  7598  dmmulpq  7599  enq0sym  7651  enq0ref  7652  enq0tr  7653  nq0nn  7661  prarloc  7722  bj-inex  16502