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  2648  2eu6  2657  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  dtruALT2  5370  exexneq  5439  dtruOLD  5446  mosubopt  5515  elopaelxpOLD  5776  ssrel  5792  ssrelOLD  5793  relopabi  5832  xpdifid  6188  ssoprab2i  7544  hash1to3  14531  catcone0  17730  isfunc  17909  umgr3v3e3cycl  30203  frgrconngr  30313  bnj605  34921  bnj607  34930  bnj916  34947  bnj996  34970  bnj907  34981  bnj1128  35004  funen1cnv  35102  cusgr3cyclex  35141  acycgrislfgr  35157  umgracycusgr  35159  cusgracyclt3v  35161  ac6s6f  38180  mnringmulrcld  44247  2uasbanh  44581  2uasbanhVD  44931  elsprel  47462  sprssspr  47468  2exopprim  47512  reuopreuprim  47513