Theorem 2eximi 1832

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

Syntax hints:   → wi 4  ∃wex 1776

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

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  2mo  2729  2eu6  2740  cgsex2g  3539  cgsex4g  3540  vtocl2OLD  3563  dtru  5264  mosubopt  5393  elopaelxp  5636  ssrel  5652  relopabi  5689  xpdifid  6020  ssoprab2i  7257  hash1to3  13843  isfunc  17128  umgr3v3e3cycl  27957  frgrconngr  28067  bnj605  32174  bnj607  32183  bnj916  32200  bnj996  32223  bnj907  32234  bnj1128  32257  funen1cnv  32352  cusgr3cyclex  32378  acycgrislfgr  32394  umgracycusgr  32396  cusgracyclt3v  32398  bj-dtru  34134  ac6s6f  35445  sn-dtru  39104  2uasbanh  40888  2uasbanhVD  41238  elsprel  43630  sprssspr  43636  2exopprim  43680  reuopreuprim  43681