Theorem 2eximdv 1949

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1864. (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
2alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
2eximdv	⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2eximdv

Step	Hyp	Ref	Expression
1		2alimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	eximdv 1947	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1947	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  2eu6  2684  cgsex2g  3500  cgsex4g  3501  spc2egv  3559  rexopabb  5514  relop  5838  elinxp  6020  opreuopreu  8032  en3  9242  en4  9243  addsrpr  11061  mulsrpr  11062  hash2prde  14509  hash3tpde  14532  pmtrrn2  19531  umgredg  29466  umgr2wlkon  30277  trsp2cyc  33421  acycgrsubgr  35628  satfvsucsuc  35835  fmla0xp  35853  fundmpss  36237  cgsex2gd  37759  pellexlem5  43540  ax6e2eq  45246  fnchoice  45729  fzisoeu  45999  stoweidlem35  46729  stoweidlem60  46754  or2expropbi  47748  ich2exprop  48197  grlimprclnbgr  48738