Theorem exlimdvv 1912

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
exlimdvv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
exlimdvv	⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥   𝜒,𝑦   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem exlimdvv

Step	Hyp	Ref	Expression
1		exlimdvv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	exlimdv 1833	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1833	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4288  funopg  5293  th3qlem1  6700  fundmen  6869  sbthlemi10  7036  addnq0mo  7519  mulnq0mo  7520  genprndl  7593  genprndu  7594  genpdisj  7595  mullocpr  7643  addsrmo  7815  mulsrmo  7816  cnm  7904  summodc  11553  fsum2dlemstep  11604  prodmodc  11748  fprod2dlemstep  11792  txbasval  14550