Theorem 2eximdv 1926

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  2eu6  2661  cgsex2g  3478  cgsex4g  3479  spc2egv  3544  rexopabb  5477  relop  5799  elinxp  5978  opreuopreu  7983  en3  9188  en4  9189  addsrpr  10996  mulsrpr  10997  hash2prde  14430  hash3tpde  14453  pmtrrn2  19433  umgredg  29232  umgr2wlkon  30043  trsp2cyc  33211  acycgrsubgr  35393  satfvsucsuc  35600  fmla0xp  35618  fundmpss  36002  cgsex2gd  37504  pellexlem5  43285  ax6e2eq  45008  fnchoice  45484  fzisoeu  45755  stoweidlem35  46485  stoweidlem60  46510  or2expropbi  47504  ich2exprop  47953  grlimprclnbgr  48494