Theorem 2eximi 1846

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

Syntax hints:   → wi 4  ∃wex 1789

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

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

This theorem is referenced by:  2mo  2665  2eu6  2673  cgsex2g  3489  cgsex4g  3490  dtruALT2  5317  exexneq  5392  mosubopt  5469  ssrel  5744  relopabi  5784  xpdifid  6139  ssoprab2i  7492  hash1to3  14491  catcone0  17691  isfunc  17869  umgr3v3e3cycl  30321  frgrconngr  30431  bnj605  35149  bnj607  35158  bnj916  35175  bnj996  35198  bnj907  35209  bnj1128  35232  funen1cnv  35329  cusgr3cyclex  35424  acycgrislfgr  35440  umgracycusgr  35442  cusgracyclt3v  35444  ac6s6f  38610  mnringmulrcld  44742  2uasbanh  45075  2uasbanhVD  45424  elsprel  48019  sprssspr  48025  2exopprim  48069  reuopreuprim  48070