Theorem exlimdvv 1884

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

Syntax hints:   → wi 4  ∃wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1434  ax-gen 1436  ax-ie2 1481  ax-17 1513

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4226  funopg  5216  th3qlem1  6594  fundmen  6763  sbthlemi10  6922  addnq0mo  7379  mulnq0mo  7380  genprndl  7453  genprndu  7454  genpdisj  7455  mullocpr  7503  addsrmo  7675  mulsrmo  7676  cnm  7764  summodc  11310  fsum2dlemstep  11361  prodmodc  11505  fprod2dlemstep  11549  txbasval  12808