Theorem 2eximi 1834

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

Syntax hints:   → wi 4  ∃wex 1777

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

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

This theorem is referenced by:  2mo  2651  2eu6  2660  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  dtruALT2  5388  exexneq  5454  dtruOLD  5461  mosubopt  5529  elopaelxpOLD  5790  ssrel  5806  ssrelOLD  5807  relopabi  5846  xpdifid  6199  ssoprab2i  7561  hash1to3  14541  catcone0  17745  isfunc  17928  umgr3v3e3cycl  30216  frgrconngr  30326  bnj605  34883  bnj607  34892  bnj916  34909  bnj996  34932  bnj907  34943  bnj1128  34966  funen1cnv  35064  cusgr3cyclex  35104  acycgrislfgr  35120  umgracycusgr  35122  cusgracyclt3v  35124  ac6s6f  38133  mnringmulrcld  44197  2uasbanh  44532  2uasbanhVD  44882  elsprel  47349  sprssspr  47355  2exopprim  47399  reuopreuprim  47400