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 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2mo  2650  2eu6  2658  cgsex2g  3475  cgsex4g  3476  cgsex4gOLD  3477  dtruALT2  5293  dtru  5359  mosubopt  5424  elopaelxpOLD  5677  ssrel  5693  ssrelOLD  5694  relopabi  5732  xpdifid  6071  ssoprab2i  7385  hash1to3  14205  catcone0  17396  isfunc  17579  umgr3v3e3cycl  28548  frgrconngr  28658  bnj605  32887  bnj607  32896  bnj916  32913  bnj996  32936  bnj907  32947  bnj1128  32970  funen1cnv  33060  cusgr3cyclex  33098  acycgrislfgr  33114  umgracycusgr  33116  cusgracyclt3v  33118  bj-dtru  34999  ac6s6f  36331  sn-dtru  40188  mnringmulrcld  41846  2uasbanh  42181  2uasbanhVD  42531  elsprel  44927  sprssspr  44933  2exopprim  44977  reuopreuprim  44978