Theorem 2eximi 1868

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

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

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

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

This theorem is used by:  2mo  2673  2eu6  2681  cgsex2g  3495  cgsex4g  3496  dtruALT2  5331  exexneq  5402  mosubopt  5481  mosubott  5483  ssrel  5758  relopabi  5799  xpdifid  6158  xpdifcnvepel  6159  ssoprab2i  7531  funen1cnv  9056  hash1to3  14637  catcone0  17861  isfunc  18039  umgr3v3e3cycl  30785  frgrconngr  30895  bnj605  35579  bnj607  35588  bnj916  35605  bnj996  35628  bnj907  35639  bnj1128  35662  cusgr3cyclex  35953  acycgrislfgr  35959  umgracycusgr  35961  cusgracyclt3v  35963  ac6s6f  39148  mnringmulrcld  45269  2uasbanh  45587  2uasbanhVD  45936  elsprel  48600  sprssspr  48606  2exopprim  48650  reuopreuprim  48651