Theorem 2eximdv 1919

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  2eu6  2657  cgsex2g  3511  cgsex4g  3512  cgsex4gOLD  3513  spc2egv  3583  rexopabb  5508  relop  5835  elinxp  6011  opreuopreu  8038  en3  9293  en4  9294  addsrpr  11094  mulsrpr  11095  hash2prde  14493  hash3tpde  14516  pmtrrn2  19446  umgredg  29122  umgr2wlkon  29937  trsp2cyc  33139  acycgrsubgr  35185  satfvsucsuc  35392  fmla0xp  35410  fundmpss  35789  pellexlem5  42823  ax6e2eq  44549  fnchoice  45020  fzisoeu  45296  stoweidlem35  46031  stoweidlem60  46056  or2expropbi  47030  ich2exprop  47452