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  2687  cgsex2g  3503  cgsex4g  3504  spc2egv  3561  rexopabb  5517  relop  5841  elinxp  6023  opreuopreu  8040  en3  9251  en4  9252  addsrpr  11078  mulsrpr  11079  hash2prde  14527  hash3tpde  14550  pmtrrn2  19561  umgredg  29525  umgr2wlkon  30336  trsp2cyc  33474  acycgrsubgr  35671  satfvsucsuc  35878  fmla0xp  35896  fundmpss  36280  cgsex2gd  37822  pellexlem5  43601  ax6e2eq  45307  fnchoice  45790  fzisoeu  46060  stoweidlem35  46790  stoweidlem60  46815  or2expropbi  47812  ich2exprop  48261  grlimprclnbgr  48802