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  6705  fundmen  6874  sbthlemi10  7041  addnq0mo  7531  mulnq0mo  7532  genprndl  7605  genprndu  7606  genpdisj  7607  mullocpr  7655  addsrmo  7827  mulsrmo  7828  cnm  7916  summodc  11565  fsum2dlemstep  11616  prodmodc  11760  fprod2dlemstep  11804  txbasval  14587