Theorem 2eximdv 1952

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2eu6  2682  cgsex2g  3496  cgsex4g  3497  spc2egv  3554  rexopabb  5502  elrelb  5775  relop  5828  elinxp  6010  opreuopreu  8035  en3  9256  en4  9257  addsrpr  11141  mulsrpr  11142  hash2prde  14595  hash3tpde  14618  pmtrrn2  19654  umgredg  29698  umgr2wlkon  30521  trsp2cyc  33666  acycgrsubgr  35892  satfvsucsuc  36099  fmla0xp  36117  fundmpss  36501  cgsex2gd  38026  pellexlem5  43793  ax6e2eq  45499  fnchoice  45989  fzisoeu  46259  stoweidlem35  46989  stoweidlem60  47014  or2expropbi  48048  ich2exprop  48497  grlimprclnbgr  49038