Theorem 2eximi 1798

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

Syntax hints:   → wi 4  ∃wex 1742

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

This theorem depends on definitions:  df-bi 199  df-ex 1743

This theorem is referenced by:  2mo  2679  2eu6  2688  cgsex2g  3459  cgsex4g  3460  vtocl2OLD  3481  dtru  5125  mosubopt  5257  elopaelxp  5492  ssrel  5508  relopabi  5545  xpdifid  5867  ssoprab2i  7081  hash1to3  13663  isfunc  16995  umgr3v3e3cycl  27716  frgrconngr  27831  bnj605  31826  bnj607  31835  bnj916  31852  bnj996  31874  bnj907  31884  bnj1128  31907  bj-dtru  33625  ac6s6f  34895  sn-dtru  38556  2uasbanh  40314  2uasbanhVD  40664  elsprel  43006  sprssspr  43012  2exopprim  43056  reuopreuprim  43057