Theorem 2eximi 1837

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

Syntax hints:   → wi 4  ∃wex 1780

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

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  2mo  2643  2eu6  2652  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  dtruALT2  5310  exexneq  5379  mosubopt  5453  ssrel  5727  relopabi  5767  xpdifid  6121  ssoprab2i  7463  hash1to3  14405  catcone0  17599  isfunc  17777  umgr3v3e3cycl  30171  frgrconngr  30281  bnj605  34926  bnj607  34935  bnj916  34952  bnj996  34975  bnj907  34986  bnj1128  35009  funen1cnv  35107  cusgr3cyclex  35187  acycgrislfgr  35203  umgracycusgr  35205  cusgracyclt3v  35207  ac6s6f  38219  mnringmulrcld  44326  2uasbanh  44659  2uasbanhVD  45008  elsprel  47580  sprssspr  47586  2exopprim  47630  reuopreuprim  47631