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  1711  cgsex2g  2839  cgsex4g  2840  vtocl2  2859  vtocl3  2860  dtruarb  4281  opelopabsb  4354  mosubopt  4791  xpmlem  5157  brabvv  6067  ssoprab2i  6110  dmaddpqlem  7597  nqpi  7598  dmaddpq  7599  dmmulpq  7600  enq0sym  7652  enq0ref  7653  enq0tr  7654  nq0nn  7662  prarloc  7723  bj-inex  16523