Theorem exlimdvv 1946

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

Syntax hints:   → wi 4  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4347  opabssxpd  4762  funopg  5360  funopsn  5830  th3qlem1  6806  fundmen  6981  sbthlemi10  7165  addnq0mo  7667  mulnq0mo  7668  genprndl  7741  genprndu  7742  genpdisj  7743  mullocpr  7791  addsrmo  7963  mulsrmo  7964  cnm  8052  summodc  11949  fsum2dlemstep  12000  prodmodc  12144  fprod2dlemstep  12188  txbasval  14997  upgr1een  15981