Theorem 2eximi 1581

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

Syntax hints:   -> wi 4   E.wex 1469

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excomim  1642  cgsex2g  2725  cgsex4g  2726  vtocl2  2744  vtocl3  2745  dtruarb  4123  opelopabsb  4190  mosubopt  4612  xpmlem  4967  brabvv  5825  ssoprab2i  5868  dmaddpqlem  7209  nqpi  7210  dmaddpq  7211  dmmulpq  7212  enq0sym  7264  enq0ref  7265  enq0tr  7266  nq0nn  7274  prarloc  7335  bj-inex  13276