Theorem 2eximi 1839

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

Syntax hints:   → wi 4  ∃wex 1782

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

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

This theorem is referenced by:  2mo  2645  2eu6  2653  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  dtruALT2  5369  exexneq  5435  dtruOLD  5442  mosubopt  5511  elopaelxpOLD  5767  ssrel  5783  ssrelOLD  5784  relopabi  5823  xpdifid  6168  ssoprab2i  7519  hash1to3  14452  catcone0  17631  isfunc  17814  umgr3v3e3cycl  29468  frgrconngr  29578  bnj605  33949  bnj607  33958  bnj916  33975  bnj996  33998  bnj907  34009  bnj1128  34032  funen1cnv  34122  cusgr3cyclex  34158  acycgrislfgr  34174  umgracycusgr  34176  cusgracyclt3v  34178  ac6s6f  37089  mnringmulrcld  43035  2uasbanh  43370  2uasbanhVD  43720  elsprel  46191  sprssspr  46197  2exopprim  46241  reuopreuprim  46242