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  3484  cgsex4g  3485  cgsex4gOLD  3486  spc2egv  3556  rexopabb  5475  relop  5797  elinxp  5974  opreuopreu  7976  en3  9185  en4  9186  addsrpr  10988  mulsrpr  10989  hash2prde  14395  hash3tpde  14418  pmtrrn2  19357  umgredg  29101  umgr2wlkon  29913  trsp2cyc  33078  acycgrsubgr  35130  satfvsucsuc  35337  fmla0xp  35355  fundmpss  35739  pellexlem5  42806  ax6e2eq  44531  fnchoice  45007  fzisoeu  45282  stoweidlem35  46017  stoweidlem60  46042  or2expropbi  47019  ich2exprop  47456  grlimprclnbgr  47981