Theorem exlimdv 1843

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

Syntax hints:   → wi 4  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1471  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1844  exlimdvv  1922  exlimddv  1923  tpid3g  3753  sssnm  3801  pwntru  4251  euotd  4307  ralxfr2d  4519  rexxfr2d  4520  releldmb  4924  relelrnb  4925  elres  5004  iss  5014  imain  5365  elunirn  5848  ovmpt4g  6081  oprssdmm  6270  op1steq  6278  fo2ndf  6326  reldmtpos  6352  rntpos  6356  tfrlemibacc  6425  tfrlemibxssdm  6426  tfrlemibfn  6427  tfrexlem  6433  tfr1onlembacc  6441  tfr1onlembxssdm  6442  tfr1onlembfn  6443  tfrcllembacc  6454  tfrcllembxssdm  6455  tfrcllembfn  6456  map0g  6788  xpdom3m  6944  phplem4  6967  phpm  6977  findcard2  7001  findcard2s  7002  ac6sfi  7010  fiintim  7043  xpfi  7044  fidcenum  7073  ordiso  7153  ctmlemr  7225  ctm  7226  ctssdc  7230  pm54.43  7313  exmidfodomrlemim  7325  iftrueb01  7354  pw1m  7355  recclnq  7525  ltexnqq  7541  ltbtwnnqq  7548  recexprlemss1l  7768  recexprlemss1u  7769  negm  9756  ioom  10425  seq3f1olemp  10682  fiinfnf1o  10953  fihashf1rn  10955  climcau  11733  summodclem2  11768  zsumdc  11770  isumz  11775  fsumf1o  11776  fisumss  11778  fsumcl2lem  11784  fsumadd  11792  fsummulc2  11834  ntrivcvgap  11934  prodmodclem2  11963  zproddc  11965  prod1dc  11972  fprodf1o  11974  fprodssdc  11976  fprodmul  11977  nnmindc  12430  uzwodc  12433  pceu  12693  4sqlemafi  12793  4sqlem12  12800  ennnfone  12871  enctlem  12878  unct  12888  gsumfzval  13298  sgrpidmndm  13327  subrngintm  14049  subrgintm  14080  islssm  14194  lss0cl  14206  islidlm  14316  eltg3  14604  tgtop  14615  tgidm  14621  tgrest  14716  tgcn  14755  xblm  14964  dvfgg  15235  dvcnp2cntop  15246  2lgslem1  15643  dom1o  16067  pwtrufal  16075