Theorem exlimdv 1833

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
exlimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
exlimdv	⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		ax-17 1540	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1540	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1610	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:  ax11v2  1834  exlimdvv  1912  exlimddv  1913  tpid3g  3737  sssnm  3784  pwntru  4232  euotd  4287  ralxfr2d  4499  rexxfr2d  4500  releldmb  4903  relelrnb  4904  elres  4982  iss  4992  imain  5340  elunirn  5813  ovmpt4g  6045  oprssdmm  6229  op1steq  6237  fo2ndf  6285  reldmtpos  6311  rntpos  6315  tfrlemibacc  6384  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrexlem  6392  tfr1onlembacc  6400  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembxssdm  6414  tfrcllembfn  6415  map0g  6747  xpdom3m  6893  phplem4  6916  phpm  6926  findcard2  6950  findcard2s  6951  ac6sfi  6959  fiintim  6992  xpfi  6993  fidcenum  7022  ordiso  7102  ctmlemr  7174  ctm  7175  ctssdc  7179  pm54.43  7257  exmidfodomrlemim  7268  recclnq  7459  ltexnqq  7475  ltbtwnnqq  7482  recexprlemss1l  7702  recexprlemss1u  7703  negm  9689  ioom  10350  seq3f1olemp  10607  fiinfnf1o  10878  fihashf1rn  10880  climcau  11512  summodclem2  11547  zsumdc  11549  isumz  11554  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  ntrivcvgap  11713  prodmodclem2  11742  zproddc  11744  prod1dc  11751  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  nnmindc  12201  uzwodc  12204  pceu  12464  4sqlemafi  12564  4sqlem12  12571  ennnfone  12642  enctlem  12649  unct  12659  gsumfzval  13034  sgrpidmndm  13061  subrngintm  13768  subrgintm  13799  islssm  13913  lss0cl  13925  islidlm  14035  eltg3  14293  tgtop  14304  tgidm  14310  tgrest  14405  tgcn  14444  xblm  14653  dvfgg  14924  dvcnp2cntop  14935  2lgslem1  15332  pwtrufal  15642