Theorem 2eximi 1830

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

Syntax hints:   → wi 4  ∃wex 1773

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

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

This theorem is referenced by:  2mo  2636  2eu6  2645  cgsex2g  3508  cgsex4g  3509  cgsex4gOLD  3510  cgsex4gOLDOLD  3511  dtruALT2  5370  exexneq  5436  dtruOLD  5443  mosubopt  5512  elopaelxpOLD  5768  ssrel  5784  ssrelOLD  5785  relopabi  5824  xpdifid  6174  ssoprab2i  7531  hash1to3  14496  catcone0  17686  isfunc  17869  umgr3v3e3cycl  30086  frgrconngr  30196  bnj605  34689  bnj607  34698  bnj916  34715  bnj996  34738  bnj907  34749  bnj1128  34772  funen1cnv  34862  cusgr3cyclex  34897  acycgrislfgr  34913  umgracycusgr  34915  cusgracyclt3v  34917  ac6s6f  37797  mnringmulrcld  43812  2uasbanh  44147  2uasbanhVD  44497  elsprel  46957  sprssspr  46963  2exopprim  47007  reuopreuprim  47008