Theorem 2eximi 1537

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

Syntax hints:   -> wi 4   E.wex 1426

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  excomim  1598  cgsex2g  2655  cgsex4g  2656  vtocl2  2674  vtocl3  2675  dtruarb  4024  opelopabsb  4085  mosubopt  4499  xpmlem  4847  brabvv  5687  ssoprab2i  5729  dmaddpqlem  6926  nqpi  6927  dmaddpq  6928  dmmulpq  6929  enq0sym  6981  enq0ref  6982  enq0tr  6983  nq0nn  6991  prarloc  7052  bj-inex  11681