Theorem exlimdvv 1897

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

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4256  funopg  5252  th3qlem1  6639  fundmen  6808  sbthlemi10  6967  addnq0mo  7448  mulnq0mo  7449  genprndl  7522  genprndu  7523  genpdisj  7524  mullocpr  7572  addsrmo  7744  mulsrmo  7745  cnm  7833  summodc  11393  fsum2dlemstep  11444  prodmodc  11588  fprod2dlemstep  11632  txbasval  13852