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  3493  cgsex4g  3494  cgsex4gOLD  3495  dtruALT2  5325  exexneq  5394  dtruOLD  5401  mosubopt  5470  elopaelxpOLD  5729  ssrel  5745  ssrelOLD  5746  relopabi  5785  xpdifid  6141  ssoprab2i  7500  hash1to3  14457  catcone0  17648  isfunc  17826  umgr3v3e3cycl  30113  frgrconngr  30223  bnj605  34897  bnj607  34906  bnj916  34923  bnj996  34946  bnj907  34957  bnj1128  34980  funen1cnv  35078  cusgr3cyclex  35123  acycgrislfgr  35139  umgracycusgr  35141  cusgracyclt3v  35143  ac6s6f  38167  mnringmulrcld  44217  2uasbanh  44551  2uasbanhVD  44900  elsprel  47476  sprssspr  47482  2exopprim  47526  reuopreuprim  47527