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  2676  2eu6  2684  cgsex2g  3499  cgsex4g  3500  dtruALT2  5336  exexneq  5407  mosubopt  5486  mosubott  5488  ssrel  5764  relopabiOLD  5806  xpdifid  6171  xpdifcnvepel  6172  ssoprab2i  7554  funen1cnv  9084  hash1to3  14664  catcone0  17890  isfunc  18068  umgr3v3e3cycl  30815  frgrconngr  30925  bnj605  35607  bnj607  35616  bnj916  35633  bnj996  35656  bnj907  35667  bnj1128  35690  cusgr3cyclex  36068  acycgrislfgr  36074  umgracycusgr  36076  cusgracyclt3v  36078  ac6s6f  39297  mnringmulrcld  45418  2uasbanh  45735  2uasbanhVD  46084  elsprel  48762  sprssspr  48768  2exopprim  48812  reuopreuprim  48813