Theorem 2eximi 1627

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

Syntax hints:   → wi 4  ∃wex 1518

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-ial 1560

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excomim  1689  cgsex2g  2816  cgsex4g  2817  vtocl2  2836  vtocl3  2837  dtruarb  4254  opelopabsb  4327  mosubopt  4761  xpmlem  5125  brabvv  6021  ssoprab2i  6064  dmaddpqlem  7532  nqpi  7533  dmaddpq  7534  dmmulpq  7535  enq0sym  7587  enq0ref  7588  enq0tr  7589  nq0nn  7597  prarloc  7658  bj-inex  16180