Theorem 2eximdv 1848

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

Syntax hints:   → wi 4  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2eu6  2558  cgsex2g  3239  cgsex4g  3240  spc2egv  3295  spc3egv  3297  relop  5272  elres  5435  en3  8197  en4  8198  addsrpr  9896  mulsrpr  9897  hash2prde  13252  pmtrrn2  17880  umgredg  26033  umgr2wlkon  26846  fundmpss  31664  pellexlem5  37397  ax6e2eq  38773  fnchoice  39188  fzisoeu  39514  stoweidlem35  40252  stoweidlem60  40277