Theorem 2eximdv 1921

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  2eu6  2658  cgsex2g  3476  cgsex4g  3477  spc2egv  3542  rexopabb  5476  relop  5799  elinxp  5978  opreuopreu  7980  en3  9184  en4  9185  addsrpr  10989  mulsrpr  10990  hash2prde  14423  hash3tpde  14446  pmtrrn2  19426  umgredg  29221  umgr2wlkon  30033  trsp2cyc  33199  acycgrsubgr  35356  satfvsucsuc  35563  fmla0xp  35581  fundmpss  35965  cgsex2gd  37467  pellexlem5  43279  ax6e2eq  45002  fnchoice  45478  fzisoeu  45751  stoweidlem35  46481  stoweidlem60  46506  or2expropbi  47494  ich2exprop  47943  grlimprclnbgr  48484