Theorem 2eximi 1837

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  2mo  2642  2eu6  2651  cgsex2g  3480  cgsex4g  3481  cgsex4gOLD  3482  dtruALT2  5306  exexneq  5375  mosubopt  5448  ssrel  5721  relopabi  5760  xpdifid  6112  ssoprab2i  7452  hash1to3  14391  catcone0  17585  isfunc  17763  umgr3v3e3cycl  30154  frgrconngr  30264  bnj605  34909  bnj607  34918  bnj916  34935  bnj996  34958  bnj907  34969  bnj1128  34992  funen1cnv  35090  cusgr3cyclex  35148  acycgrislfgr  35164  umgracycusgr  35166  cusgracyclt3v  35168  ac6s6f  38192  mnringmulrcld  44240  2uasbanh  44573  2uasbanhVD  44922  elsprel  47485  sprssspr  47491  2exopprim  47535  reuopreuprim  47536