Theorem 2eximdv 1919

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2eu6  2650  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  spc2egv  3565  rexopabb  5488  relop  5814  elinxp  5990  opreuopreu  8013  en3  9227  en4  9228  addsrpr  11028  mulsrpr  11029  hash2prde  14435  hash3tpde  14458  pmtrrn2  19390  umgredg  29065  umgr2wlkon  29880  trsp2cyc  33080  acycgrsubgr  35145  satfvsucsuc  35352  fmla0xp  35370  fundmpss  35754  pellexlem5  42821  ax6e2eq  44547  fnchoice  45023  fzisoeu  45298  stoweidlem35  46033  stoweidlem60  46058  or2expropbi  47032  ich2exprop  47469