Theorem 2eximi 1654

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

Syntax hints:   -> wi 4   E.wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1715  cgsex2g  2858  cgsex4g  2859  vtocl2  2878  vtocl3  2879  dtruarb  4323  opelopabsb  4397  mosubopt  4835  xpmlem  5203  brabvv  6124  ssoprab2i  6167  dmaddpqlem  7734  nqpi  7735  dmaddpq  7736  dmmulpq  7737  enq0sym  7789  enq0ref  7790  enq0tr  7791  nq0nn  7799  prarloc  7860  bj-inex  16847