Theorem 2eximdv 1916

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1830. (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 1914	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1914	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

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

This theorem is referenced by:  2eu6  2740  cgsex2g  3539  cgsex4g  3540  spc2egv  3600  rexopabb  5408  relop  5716  elinxp  5885  opreuopreu  7728  en3  8749  en4  8750  addsrpr  10491  mulsrpr  10492  hash2prde  13822  pmtrrn2  18582  umgredg  26917  umgr2wlkon  27723  trsp2cyc  30760  acycgrsubgr  32400  satfvsucsuc  32607  fmla0xp  32625  fundmpss  33004  pellexlem5  39423  ax6e2eq  40884  fnchoice  41279  fzisoeu  41559  stoweidlem35  42313  stoweidlem60  42338  or2expropbi  43262  ich2exprop  43626