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  2683  cgsex2g  3498  cgsex4g  3499  spc2egv  3556  rexopabb  5510  relop  5834  elinxp  6016  opreuopreu  8035  en3  9255  en4  9256  addsrpr  11088  mulsrpr  11089  hash2prde  14539  hash3tpde  14562  pmtrrn2  19593  umgredg  29603  umgr2wlkon  30426  trsp2cyc  33571  acycgrsubgr  35745  satfvsucsuc  35952  fmla0xp  35970  fundmpss  36354  cgsex2gd  37897  pellexlem5  43682  ax6e2eq  45388  fnchoice  45871  fzisoeu  46141  stoweidlem35  46871  stoweidlem60  46896  or2expropbi  47930  ich2exprop  48379  grlimprclnbgr  48920