Theorem 2eximi 1836

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  2mo  2641  2eu6  2650  cgsex2g  3479  cgsex4g  3480  cgsex4gOLD  3481  dtruALT2  5305  exexneq  5374  mosubopt  5447  ssrel  5720  relopabi  5759  xpdifid  6111  ssoprab2i  7451  hash1to3  14387  catcone0  17580  isfunc  17758  umgr3v3e3cycl  30115  frgrconngr  30225  bnj605  34887  bnj607  34896  bnj916  34913  bnj996  34936  bnj907  34947  bnj1128  34970  funen1cnv  35068  cusgr3cyclex  35126  acycgrislfgr  35142  umgracycusgr  35144  cusgracyclt3v  35146  ac6s6f  38170  mnringmulrcld  44218  2uasbanh  44551  2uasbanhVD  44900  elsprel  47473  sprssspr  47479  2exopprim  47523  reuopreuprim  47524