Theorem 2eximdv 1942

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

Syntax hints:   → wi 4  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  2eu6  2686  cgsex2g  3502  cgsex4g  3503  spc2egv  3561  rexopabb  5503  relop  5827  elinxp  6009  opreuopreu  8019  en3  9229  en4  9230  addsrpr  11048  mulsrpr  11049  hash2prde  14497  hash3tpde  14520  pmtrrn2  19521  umgredg  29397  umgr2wlkon  30208  trsp2cyc  33356  acycgrsubgr  35521  satfvsucsuc  35728  fmla0xp  35746  fundmpss  36130  cgsex2gd  37641  pellexlem5  43422  ax6e2eq  45131  fnchoice  45607  fzisoeu  45877  stoweidlem35  46607  stoweidlem60  46632  or2expropbi  47626  ich2exprop  48075  grlimprclnbgr  48616