Theorem 2eximi 1838

Description: Inference adding two 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 1837	. 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓)
3	2	eximi 1837	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  2mo  2649  2eu6  2658  cgsex2g  3476  cgsex4g  3477  dtruALT2  5313  exexneq  5388  mosubopt  5465  ssrel  5739  relopabi  5778  xpdifid  6133  ssoprab2i  7478  hash1to3  14454  catcone0  17653  isfunc  17831  umgr3v3e3cycl  30254  frgrconngr  30364  bnj605  35049  bnj607  35058  bnj916  35075  bnj996  35098  bnj907  35109  bnj1128  35132  funen1cnv  35231  cusgr3cyclex  35318  acycgrislfgr  35334  umgracycusgr  35336  cusgracyclt3v  35338  ac6s6f  38494  mnringmulrcld  44655  2uasbanh  44988  2uasbanhVD  45337  elsprel  47929  sprssspr  47935  2exopprim  47979  reuopreuprim  47980