Theorem 2eximi 1594

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

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excomim  1656  cgsex2g  2766  cgsex4g  2767  vtocl2  2785  vtocl3  2786  dtruarb  4177  opelopabsb  4245  mosubopt  4676  xpmlem  5031  brabvv  5899  ssoprab2i  5942  dmaddpqlem  7339  nqpi  7340  dmaddpq  7341  dmmulpq  7342  enq0sym  7394  enq0ref  7395  enq0tr  7396  nq0nn  7404  prarloc  7465  bj-inex  13942