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  2657  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  spc2egv  3599  rexopabb  5533  relop  5861  elinxp  6037  opreuopreu  8059  en3  9316  en4  9317  addsrpr  11115  mulsrpr  11116  hash2prde  14509  hash3tpde  14532  pmtrrn2  19478  umgredg  29155  umgr2wlkon  29970  trsp2cyc  33143  acycgrsubgr  35163  satfvsucsuc  35370  fmla0xp  35388  fundmpss  35767  pellexlem5  42844  ax6e2eq  44577  fnchoice  45034  fzisoeu  45312  stoweidlem35  46050  stoweidlem60  46075  or2expropbi  47046  ich2exprop  47458