Theorem 2eximi 1611

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 1610	. 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓)
3	2	eximi 1610	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Syntax hints:   → wi 4  ∃wex 1502

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-ial 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1673  cgsex2g  2785  cgsex4g  2786  vtocl2  2804  vtocl3  2805  dtruarb  4203  opelopabsb  4272  mosubopt  4703  xpmlem  5061  brabvv  5934  ssoprab2i  5977  dmaddpqlem  7390  nqpi  7391  dmaddpq  7392  dmmulpq  7393  enq0sym  7445  enq0ref  7446  enq0tr  7447  nq0nn  7455  prarloc  7516  bj-inex  14955