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  3476  cgsex4g  3477  dtruALT2  5305  exexneq  5380  mosubopt  5456  ssrel  5730  relopabi  5769  xpdifid  6124  ssoprab2i  7469  hash1to3  14416  catcone0  17611  isfunc  17789  umgr3v3e3cycl  30243  frgrconngr  30353  bnj605  35055  bnj607  35064  bnj916  35081  bnj996  35104  bnj907  35115  bnj1128  35138  funen1cnv  35237  cusgr3cyclex  35324  acycgrislfgr  35340  umgracycusgr  35342  cusgracyclt3v  35344  ac6s6f  38485  mnringmulrcld  44658  2uasbanh  44991  2uasbanhVD  45340  elsprel  47909  sprssspr  47915  2exopprim  47959  reuopreuprim  47960