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 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used by:  excomim  1715  cgsex2g  2858  cgsex4g  2859  vtocl2  2878  vtocl3  2879  dtruarb  4330  opelopabsb  4404  mosubopt  4842  xpmlem  5211  brabvv  6137  ssoprab2i  6180  dmaddpqlem  7751  nqpi  7752  dmaddpq  7753  dmmulpq  7754  enq0sym  7806  enq0ref  7807  enq0tr  7808  nq0nn  7816  prarloc  7877  bj-inex  17150