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  2647  2eu6  2656  cgsex2g  3473  cgsex4g  3474  dtruALT2  5301  exexneq  5376  mosubopt  5453  ssrel  5728  relopabi  5767  xpdifid  6121  ssoprab2i  7467  hash1to3  14443  catcone0  17642  isfunc  17820  umgr3v3e3cycl  30242  frgrconngr  30352  bnj605  35037  bnj607  35046  bnj916  35063  bnj996  35086  bnj907  35097  bnj1128  35120  funen1cnv  35219  cusgr3cyclex  35306  acycgrislfgr  35322  umgracycusgr  35324  cusgracyclt3v  35326  ac6s6f  38482  mnringmulrcld  44643  2uasbanh  44976  2uasbanhVD  45325  elsprel  47923  sprssspr  47929  2exopprim  47973  reuopreuprim  47974