Theorem 2eximdv 1888

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

Syntax hints:   → wi 4  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

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

This theorem is referenced by:  2eu6  2587  cgsex2g  3270  cgsex4g  3271  spc2egv  3326  spc3egv  3328  relop  5305  elres  5470  en3  8238  en4  8239  addsrpr  9934  mulsrpr  9935  hash2prde  13290  pmtrrn2  17926  umgredg  26078  umgr2wlkon  26915  fundmpss  31790  pellexlem5  37714  ax6e2eq  39090  fnchoice  39502  fzisoeu  39828  stoweidlem35  40570  stoweidlem60  40595