Theorem 2eximdv 1921

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 1919	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1919	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 1912

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

This theorem is referenced by:  2eu6  2658  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spc2egv  3555  rexopabb  5484  relop  5807  elinxp  5986  opreuopreu  7988  en3  9193  en4  9194  addsrpr  10998  mulsrpr  10999  hash2prde  14405  hash3tpde  14428  pmtrrn2  19401  umgredg  29223  umgr2wlkon  30035  trsp2cyc  33216  acycgrsubgr  35371  satfvsucsuc  35578  fmla0xp  35596  fundmpss  35980  cgsex2gd  37386  pellexlem5  43184  ax6e2eq  44907  fnchoice  45383  fzisoeu  45656  stoweidlem35  46387  stoweidlem60  46412  or2expropbi  47388  ich2exprop  47825  grlimprclnbgr  48350