Theorem 2eximi 1532

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

Syntax hints:   -> wi 4   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  excomim  1593  cgsex2g  2635  cgsex4g  2636  vtocl2  2654  vtocl3  2655  dtruarb  3962  opelopabsb  4015  mosubopt  4423  xpmlem  4764  brabvv  5571  ssoprab2i  5613  dmaddpqlem  6567  nqpi  6568  dmaddpq  6569  dmmulpq  6570  enq0sym  6622  enq0ref  6623  enq0tr  6624  nq0nn  6632  prarloc  6693  bj-inex  10698