Theorem 2eximdv 1835

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

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2eu6  2546  cgsex2g  3212  cgsex4g  3213  spc2egv  3268  spc3egv  3270  relop  5194  elres  5355  en3  8082  en4  8083  addsrpr  9775  mulsrpr  9776  hash2prde  13109  pmtrrn2  17703  umgredg  25812  usgrarnedg  25913  fundmpss  30910  pellexlem5  36415  ax6e2eq  37794  fnchoice  38211  fzisoeu  38455  stoweidlem35  38928  stoweidlem60  38953  umgr2wlkon  41157