Theorem 2eximi 1865

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1808

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ex 1809

This theorem is used by:  2mo  2675  2eu6  2683  cgsex2g  3499  cgsex4g  3500  dtruALT2  5340  exexneq  5415  mosubopt  5492  ssrel  5768  relopabi  5808  xpdifid  6164  xpdifcnvepel  6165  ssoprab2i  7523  hash1to3  14536  catcone0  17749  isfunc  17927  umgr3v3e3cycl  30546  frgrconngr  30656  bnj605  35304  bnj607  35313  bnj916  35330  bnj996  35353  bnj907  35364  bnj1128  35387  funen1cnv  35486  cusgr3cyclex  35636  acycgrislfgr  35652  umgracycusgr  35654  cusgracyclt3v  35656  ac6s6f  38850  mnringmulrcld  44980  2uasbanh  45298  2uasbanhVD  45647  elsprel  48252  sprssspr  48258  2exopprim  48302  reuopreuprim  48303