Theorem 2eximdv 1922

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  2eu6  2652  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  spc2egv  3589  rexopabb  5528  relop  5850  elinxp  6019  opreuopreu  8019  en3  9281  en4  9282  addsrpr  11069  mulsrpr  11070  hash2prde  14430  pmtrrn2  19327  umgredg  28395  umgr2wlkon  29201  trsp2cyc  32277  acycgrsubgr  34144  satfvsucsuc  34351  fmla0xp  34369  fundmpss  34733  pellexlem5  41561  ax6e2eq  43308  fnchoice  43703  fzisoeu  44000  stoweidlem35  44741  stoweidlem60  44766  or2expropbi  45734  ich2exprop  46129