Theorem 2eximi 1650

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

Syntax hints:   -> wi 4   E.wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1711  cgsex2g  2850  cgsex4g  2851  vtocl2  2870  vtocl3  2871  dtruarb  4304  opelopabsb  4378  mosubopt  4815  xpmlem  5183  brabvv  6099  ssoprab2i  6142  dmaddpqlem  7692  nqpi  7693  dmaddpq  7694  dmmulpq  7695  enq0sym  7747  enq0ref  7748  enq0tr  7749  nq0nn  7757  prarloc  7818  bj-inex  16677