Theorem 2eximi 1836

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  2mo  2642  2eu6  2650  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  dtruALT2  5369  exexneq  5435  dtruOLD  5442  mosubopt  5511  elopaelxpOLD  5767  ssrel  5783  ssrelOLD  5784  relopabi  5823  xpdifid  6168  ssoprab2i  7523  hash1to3  14458  catcone0  17637  isfunc  17820  umgr3v3e3cycl  29702  frgrconngr  29812  bnj605  34214  bnj607  34223  bnj916  34240  bnj996  34263  bnj907  34274  bnj1128  34297  funen1cnv  34387  cusgr3cyclex  34423  acycgrislfgr  34439  umgracycusgr  34441  cusgracyclt3v  34443  ac6s6f  37346  mnringmulrcld  43291  2uasbanh  43626  2uasbanhVD  43976  elsprel  46443  sprssspr  46449  2exopprim  46493  reuopreuprim  46494