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 206  df-ex 1781

This theorem is referenced by:  2mo  2648  2eu6  2656  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  dtruALT2  5310  exexneq  5376  dtruOLD  5383  mosubopt  5448  elopaelxpOLD  5702  ssrel  5718  ssrelOLD  5719  relopabi  5758  xpdifid  6100  ssoprab2i  7439  hash1to3  14297  catcone0  17485  isfunc  17668  umgr3v3e3cycl  28777  frgrconngr  28887  bnj605  33127  bnj607  33136  bnj916  33153  bnj996  33176  bnj907  33187  bnj1128  33210  funen1cnv  33300  cusgr3cyclex  33338  acycgrislfgr  33354  umgracycusgr  33356  cusgracyclt3v  33358  ac6s6f  36429  mnringmulrcld  42156  2uasbanh  42491  2uasbanhVD  42841  elsprel  45267  sprssspr  45273  2exopprim  45317  reuopreuprim  45318