Theorem 2eximdv 1923

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

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  2eu6  2658  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  spc2egv  3528  rexopabb  5434  relop  5748  elinxp  5918  opreuopreu  7849  en3  8984  en4  8985  addsrpr  10762  mulsrpr  10763  hash2prde  14112  pmtrrn2  18983  umgredg  27411  umgr2wlkon  28216  trsp2cyc  31292  acycgrsubgr  33020  satfvsucsuc  33227  fmla0xp  33245  fundmpss  33646  pellexlem5  40571  ax6e2eq  42066  fnchoice  42461  fzisoeu  42729  stoweidlem35  43466  stoweidlem60  43491  or2expropbi  44415  ich2exprop  44811