Theorem 2eximi 1601

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

Syntax hints:   → wi 4  ∃wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1663  cgsex2g  2775  cgsex4g  2776  vtocl2  2794  vtocl3  2795  dtruarb  4193  opelopabsb  4262  mosubopt  4693  xpmlem  5051  brabvv  5923  ssoprab2i  5966  dmaddpqlem  7378  nqpi  7379  dmaddpq  7380  dmmulpq  7381  enq0sym  7433  enq0ref  7434  enq0tr  7435  nq0nn  7443  prarloc  7504  bj-inex  14698