Theorem 2eximi 1857

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

Syntax hints:   → wi 4  ∃wex 1800

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

This theorem depends on definitions:  df-bi 209  df-ex 1801

This theorem is referenced by:  2mo  2676  2eu6  2684  cgsex2g  3500  cgsex4g  3501  dtruALT2  5328  exexneq  5403  mosubopt  5480  ssrel  5756  relopabi  5796  xpdifid  6153  xpdifcnvepel  6154  ssoprab2i  7507  hash1to3  14515  catcone0  17729  isfunc  17907  umgr3v3e3cycl  30393  frgrconngr  30503  bnj605  35204  bnj607  35213  bnj916  35230  bnj996  35253  bnj907  35264  bnj1128  35287  funen1cnv  35384  cusgr3cyclex  35491  acycgrislfgr  35507  umgracycusgr  35509  cusgracyclt3v  35511  ac6s6f  38677  mnringmulrcld  44809  2uasbanh  45128  2uasbanhVD  45477  elsprel  48072  sprssspr  48078  2exopprim  48122  reuopreuprim  48123