Theorem exlimdvv 1836

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 1758	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1758	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1391  ax-gen 1393  ax-ie2 1438  ax-17 1474

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4114  funopg  5093  th3qlem1  6461  fundmen  6630  sbthlemi10  6782  addnq0mo  7156  mulnq0mo  7157  genprndl  7230  genprndu  7231  genpdisj  7232  mullocpr  7280  addsrmo  7439  mulsrmo  7440  summodc  10991  fsum2dlemstep  11042  txbasval  12217