Theorem 2eximi 1869

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

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

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

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

This theorem is used by:  2mo  2675  2eu6  2683  cgsex2g  3498  cgsex4g  3499  dtruALT2  5339  exexneq  5414  mosubopt  5491  ssrel  5767  relopabi  5807  xpdifid  6164  xpdifcnvepel  6165  ssoprab2i  7527  funen1cnv  9038  hash1to3  14559  catcone0  17779  isfunc  17957  umgr3v3e3cycl  30650  frgrconngr  30760  bnj605  35403  bnj607  35412  bnj916  35429  bnj996  35452  bnj907  35463  bnj1128  35486  cusgr3cyclex  35712  acycgrislfgr  35718  umgracycusgr  35720  cusgracyclt3v  35722  ac6s6f  38908  mnringmulrcld  45053  2uasbanh  45371  2uasbanhVD  45720  elsprel  48362  sprssspr  48368  2exopprim  48412  reuopreuprim  48413