Theorem 2eximdv 1951

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  2eu6  2681  cgsex2g  3495  cgsex4g  3496  spc2egv  3553  rexopabb  5501  elrelb  5774  relop  5827  elinxp  6007  opreuopreu  8046  en3  9275  en4  9276  addsrpr  11163  mulsrpr  11164  hash2prde  14618  hash3tpde  14641  pmtrrn2  19679  umgredg  29721  umgr2wlkon  30544  trsp2cyc  33730  acycgrsubgr  35999  satfvsucsuc  36216  fmla0xp  36234  fundmpss  36624  cgsex2gd  38151  pellexlem5  43933  ax6e2eq  45633  fnchoice  46139  fzisoeu  46409  stoweidlem35  47138  stoweidlem60  47163  or2expropbi  48197  ich2exprop  48646  grlimprclnbgr  49187