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  7471  hash1to3  14419  catcone0  17614  isfunc  17792  umgr3v3e3cycl  30242  frgrconngr  30352  bnj605  35044  bnj607  35053  bnj916  35070  bnj996  35093  bnj907  35104  bnj1128  35127  funen1cnv  35225  cusgr3cyclex  35311  acycgrislfgr  35327  umgracycusgr  35329  cusgracyclt3v  35331  ac6s6f  38345  mnringmulrcld  44505  2uasbanh  44838  2uasbanhVD  45187  elsprel  47757  sprssspr  47763  2exopprim  47807  reuopreuprim  47808