Theorem 2eximi 1615

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

Syntax hints:   -> wi 4   E.wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1677  cgsex2g  2799  cgsex4g  2800  vtocl2  2819  vtocl3  2820  dtruarb  4224  opelopabsb  4294  mosubopt  4728  xpmlem  5090  brabvv  5968  ssoprab2i  6011  dmaddpqlem  7444  nqpi  7445  dmaddpq  7446  dmmulpq  7447  enq0sym  7499  enq0ref  7500  enq0tr  7501  nq0nn  7509  prarloc  7570  bj-inex  15553