Theorem 2eximi 1580

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

Syntax hints:   -> wi 4   E.wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excomim  1641  cgsex2g  2717  cgsex4g  2718  vtocl2  2736  vtocl3  2737  dtruarb  4110  opelopabsb  4177  mosubopt  4599  xpmlem  4954  brabvv  5810  ssoprab2i  5853  dmaddpqlem  7178  nqpi  7179  dmaddpq  7180  dmmulpq  7181  enq0sym  7233  enq0ref  7234  enq0tr  7235  nq0nn  7243  prarloc  7304  bj-inex  13094