Theorem 2eximi 1625

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

Syntax hints:   → wi 4  ∃wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1687  cgsex2g  2809  cgsex4g  2810  vtocl2  2829  vtocl3  2830  dtruarb  4239  opelopabsb  4310  mosubopt  4744  xpmlem  5108  brabvv  5998  ssoprab2i  6041  dmaddpqlem  7497  nqpi  7498  dmaddpq  7499  dmmulpq  7500  enq0sym  7552  enq0ref  7553  enq0tr  7554  nq0nn  7562  prarloc  7623  bj-inex  15917