Theorem 2eximi 1833

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 207  df-ex 1777

This theorem is referenced by:  2mo  2646  2eu6  2655  cgsex2g  3525  cgsex4g  3526  cgsex4gOLD  3527  dtruALT2  5376  exexneq  5445  dtruOLD  5452  mosubopt  5520  elopaelxpOLD  5779  ssrel  5795  ssrelOLD  5796  relopabi  5835  xpdifid  6190  ssoprab2i  7544  hash1to3  14528  catcone0  17732  isfunc  17915  umgr3v3e3cycl  30213  frgrconngr  30323  bnj605  34900  bnj607  34909  bnj916  34926  bnj996  34949  bnj907  34960  bnj1128  34983  funen1cnv  35081  cusgr3cyclex  35121  acycgrislfgr  35137  umgracycusgr  35139  cusgracyclt3v  35141  ac6s6f  38160  mnringmulrcld  44224  2uasbanh  44559  2uasbanhVD  44909  elsprel  47400  sprssspr  47406  2exopprim  47450  reuopreuprim  47451