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  3487  cgsex4g  3488  cgsex4gOLD  3489  dtruALT2  5316  exexneq  5385  mosubopt  5459  ssrel  5733  relopabi  5772  xpdifid  6127  ssoprab2i  7472  hash1to3  14420  catcone0  17615  isfunc  17793  umgr3v3e3cycl  30264  frgrconngr  30374  bnj605  35076  bnj607  35085  bnj916  35102  bnj996  35125  bnj907  35136  bnj1128  35159  funen1cnv  35257  cusgr3cyclex  35343  acycgrislfgr  35359  umgracycusgr  35361  cusgracyclt3v  35363  ac6s6f  38387  mnringmulrcld  44547  2uasbanh  44880  2uasbanhVD  45229  elsprel  47798  sprssspr  47804  2exopprim  47848  reuopreuprim  47849