Theorem exlimdv 1841

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 1548	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1548	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1618	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1469  ax-gen 1471  ax-ie2 1516  ax-17 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1842  exlimdvv  1920  exlimddv  1921  tpid3g  3747  sssnm  3794  pwntru  4242  euotd  4297  ralxfr2d  4509  rexxfr2d  4510  releldmb  4913  relelrnb  4914  elres  4992  iss  5002  imain  5350  elunirn  5825  ovmpt4g  6058  oprssdmm  6247  op1steq  6255  fo2ndf  6303  reldmtpos  6329  rntpos  6333  tfrlemibacc  6402  tfrlemibxssdm  6403  tfrlemibfn  6404  tfrexlem  6410  tfr1onlembacc  6418  tfr1onlembxssdm  6419  tfr1onlembfn  6420  tfrcllembacc  6431  tfrcllembxssdm  6432  tfrcllembfn  6433  map0g  6765  xpdom3m  6911  phplem4  6934  phpm  6944  findcard2  6968  findcard2s  6969  ac6sfi  6977  fiintim  7010  xpfi  7011  fidcenum  7040  ordiso  7120  ctmlemr  7192  ctm  7193  ctssdc  7197  pm54.43  7280  exmidfodomrlemim  7291  recclnq  7487  ltexnqq  7503  ltbtwnnqq  7510  recexprlemss1l  7730  recexprlemss1u  7731  negm  9718  ioom  10384  seq3f1olemp  10641  fiinfnf1o  10912  fihashf1rn  10914  climcau  11577  summodclem2  11612  zsumdc  11614  isumz  11619  fsumf1o  11620  fisumss  11622  fsumcl2lem  11628  fsumadd  11636  fsummulc2  11678  ntrivcvgap  11778  prodmodclem2  11807  zproddc  11809  prod1dc  11816  fprodf1o  11818  fprodssdc  11820  fprodmul  11821  nnmindc  12274  uzwodc  12277  pceu  12537  4sqlemafi  12637  4sqlem12  12644  ennnfone  12715  enctlem  12722  unct  12732  gsumfzval  13141  sgrpidmndm  13170  subrngintm  13892  subrgintm  13923  islssm  14037  lss0cl  14049  islidlm  14159  eltg3  14447  tgtop  14458  tgidm  14464  tgrest  14559  tgcn  14598  xblm  14807  dvfgg  15078  dvcnp2cntop  15089  2lgslem1  15486  pwtrufal  15798