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 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 210  df-ex 1782

This theorem is referenced by:  2mo  2710  2eu6  2719  cgsex2g  3485  cgsex4g  3486  cgsex4gOLD  3487  vtocl2OLD  3510  dtru  5236  mosubopt  5365  elopaelxp  5605  ssrel  5621  relopabi  5658  xpdifid  5992  ssoprab2i  7242  hash1to3  13845  isfunc  17126  umgr3v3e3cycl  27969  frgrconngr  28079  bnj605  32289  bnj607  32298  bnj916  32315  bnj996  32338  bnj907  32349  bnj1128  32372  funen1cnv  32467  cusgr3cyclex  32496  acycgrislfgr  32512  umgracycusgr  32514  cusgracyclt3v  32516  bj-dtru  34254  ac6s6f  35611  sn-dtru  39403  mnringmulrcld  40936  2uasbanh  41267  2uasbanhVD  41617  elsprel  43992  sprssspr  43998  2exopprim  44042  reuopreuprim  44043