Theorem 2eximi 1563

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

Syntax hints:   → wi 4  ∃wex 1451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excomim  1624  cgsex2g  2693  cgsex4g  2694  vtocl2  2712  vtocl3  2713  dtruarb  4075  opelopabsb  4142  mosubopt  4564  xpmlem  4917  brabvv  5771  ssoprab2i  5814  dmaddpqlem  7133  nqpi  7134  dmaddpq  7135  dmmulpq  7136  enq0sym  7188  enq0ref  7189  enq0tr  7190  nq0nn  7198  prarloc  7259  bj-inex  12797