Theorem 2eximi 1654

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

Syntax hints:   → wi 4  ∃wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1715  cgsex2g  2858  cgsex4g  2859  vtocl2  2878  vtocl3  2879  dtruarb  4326  opelopabsb  4400  mosubopt  4838  xpmlem  5206  brabvv  6128  ssoprab2i  6171  dmaddpqlem  7738  nqpi  7739  dmaddpq  7740  dmmulpq  7741  enq0sym  7793  enq0ref  7794  enq0tr  7795  nq0nn  7803  prarloc  7864  bj-inex  16916