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  2673  2eu6  2681  cgsex2g  3495  cgsex4g  3496  dtruALT2  5331  exexneq  5402  mosubopt  5479  ssrel  5755  relopabi  5796  xpdifid  6154  xpdifcnvepel  6155  ssoprab2i  7519  funen1cnv  9034  hash1to3  14604  catcone0  17822  isfunc  18000  umgr3v3e3cycl  30718  frgrconngr  30828  bnj605  35471  bnj607  35480  bnj916  35497  bnj996  35520  bnj907  35531  bnj1128  35554  cusgr3cyclex  35832  acycgrislfgr  35838  umgracycusgr  35840  cusgracyclt3v  35842  ac6s6f  39025  mnringmulrcld  45170  2uasbanh  45488  2uasbanhVD  45837  elsprel  48479  sprssspr  48485  2exopprim  48529  reuopreuprim  48530