Theorem 2eximi 1836

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  2mo  2647  2eu6  2656  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  dtruALT2  5340  exexneq  5409  dtruOLD  5416  mosubopt  5485  elopaelxpOLD  5745  ssrel  5761  ssrelOLD  5762  relopabi  5801  xpdifid  6157  ssoprab2i  7518  hash1to3  14510  catcone0  17699  isfunc  17877  umgr3v3e3cycl  30165  frgrconngr  30275  bnj605  34938  bnj607  34947  bnj916  34964  bnj996  34987  bnj907  34998  bnj1128  35021  funen1cnv  35119  cusgr3cyclex  35158  acycgrislfgr  35174  umgracycusgr  35176  cusgracyclt3v  35178  ac6s6f  38197  mnringmulrcld  44252  2uasbanh  44586  2uasbanhVD  44935  elsprel  47489  sprssspr  47495  2exopprim  47539  reuopreuprim  47540