Theorem 2eximi 1649

Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
eximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2eximi	⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Proof of Theorem 2eximi

Step	Hyp	Ref	Expression
1		eximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	eximi 1648	. 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓)
3	2	eximi 1648	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Syntax hints:   → wi 4  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1710  cgsex2g  2838  cgsex4g  2839  vtocl2  2858  vtocl3  2859  dtruarb  4283  opelopabsb  4356  mosubopt  4793  xpmlem  5159  brabvv  6072  ssoprab2i  6115  dmaddpqlem  7602  nqpi  7603  dmaddpq  7604  dmmulpq  7605  enq0sym  7657  enq0ref  7658  enq0tr  7659  nq0nn  7667  prarloc  7728  bj-inex  16562