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  1710  cgsex2g  2838  cgsex4g  2839  vtocl2  2858  vtocl3  2859  dtruarb  4280  opelopabsb  4353  mosubopt  4790  xpmlem  5156  brabvv  6069  ssoprab2i  6112  dmaddpqlem  7599  nqpi  7600  dmaddpq  7601  dmmulpq  7602  enq0sym  7654  enq0ref  7655  enq0tr  7656  nq0nn  7664  prarloc  7725  bj-inex  16560