Theorem 2eximi 1864

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

Syntax hints:   → wi 4  ∃wex 1807

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

This theorem depends on definitions:  df-bi 210  df-ex 1808

This theorem is referenced by:  2mo  2674  2eu6  2682  cgsex2g  3498  cgsex4g  3499  dtruALT2  5341  exexneq  5416  mosubopt  5493  ssrel  5769  relopabi  5809  xpdifid  6165  xpdifcnvepel  6166  ssoprab2i  7521  hash1to3  14528  catcone0  17742  isfunc  17920  umgr3v3e3cycl  30501  frgrconngr  30611  bnj605  35261  bnj607  35270  bnj916  35287  bnj996  35310  bnj907  35321  bnj1128  35344  funen1cnv  35441  cusgr3cyclex  35582  acycgrislfgr  35598  umgracycusgr  35600  cusgracyclt3v  35602  ac6s6f  38768  mnringmulrcld  44900  2uasbanh  45218  2uasbanhVD  45567  elsprel  48169  sprssspr  48175  2exopprim  48219  reuopreuprim  48220