Theorem 2eximdv 1921

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

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

This theorem is referenced by:  2eu6  2656  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  spc2egv  3547  rexopabb  5473  relop  5793  elinxp  5962  opreuopreu  7945  en3  9148  en4  9149  addsrpr  10933  mulsrpr  10934  hash2prde  14285  pmtrrn2  19165  umgredg  27798  umgr2wlkon  28604  trsp2cyc  31677  acycgrsubgr  33419  satfvsucsuc  33626  fmla0xp  33644  fundmpss  34026  pellexlem5  40968  ax6e2eq  42550  fnchoice  42945  fzisoeu  43226  stoweidlem35  43964  stoweidlem60  43989  or2expropbi  44946  ich2exprop  45341