Theorem 2eximi 1763

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

Syntax hints:   → wi 4  ∃wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2mo  2551  2eu6  2558  cgsex2g  3239  cgsex4g  3240  vtocl2  3261  vtocl3  3262  dtru  4857  mosubopt  4972  elopaelxp  5191  ssrel  5207  relopabi  5245  xpdifid  5562  ssoprab2i  6749  hash1to3  13273  isfunc  16524  umgr3v3e3cycl  27044  frgrconngr  27158  bnj605  30977  bnj607  30986  bnj916  31003  bnj996  31025  bnj907  31035  bnj1128  31058  bj-dtru  32797  ac6s6f  33981  2uasbanh  38777  2uasbanhVD  39147  elsprel  41725  sprssspr  41731