Theorem exlimdvv 1953

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  euotd  4397  opabssxpd  4813  funopg  5414  funopsn  5894  th3qlem1  6915  fundmen  7099  sbthlemi10  7289  addnq0mo  7821  mulnq0mo  7822  genprndl  7895  genprndu  7896  genpdisj  7897  mullocpr  7945  addsrmo  8117  mulsrmo  8118  cnm  8206  summodc  12176  fsum2dlemstep  12227  prodmodc  12371  fprod2dlemstep  12415  gsum2d2fi  14275  txbasval  15505  upgr1een  16582