Theorem exlimdv 1872

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

Syntax hints:   → wi 4  ∃wex 1545

This theorem was proved from 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 theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1873  exlimdvv  1953  exlimddv  1954  tpid3g  3823  sssnm  3874  pwntru  4331  euotd  4390  ralxfr2d  4605  rexxfr2d  4606  reldmm  4995  releldmb  5014  relelrnb  5015  elres  5094  iss  5104  imain  5458  elunirn  5962  ovmpt4g  6201  oprssdmm  6395  op1steq  6403  fo2ndf  6453  reldmtpos  6514  rntpos  6518  tfrlemibacc  6587  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrexlem  6595  tfr1onlembacc  6603  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfrcllembacc  6616  tfrcllembxssdm  6617  tfrcllembfn  6618  map0g  6959  dom1o  7106  xpdom3m  7122  phplem4  7146  phpm  7157  findcard2  7183  findcard2s  7184  ac6sfi  7192  fiintim  7228  xpfi  7229  fidcenum  7263  ordiso  7366  ctmlemr  7438  ctm  7439  ctssdc  7443  pm54.43  7526  exmidfodomrlemim  7543  iftrueb01  7572  pw1m  7573  recclnq  7749  ltexnqq  7765  ltbtwnnqq  7772  recexprlemss1l  7992  recexprlemss1u  7993  negm  9994  ioom  10673  seq3f1olemp  10930  fiinfnf1o  11203  fihashf1rn  11205  hashf1  11265  climcau  12091  summodclem2  12127  zsumdc  12129  isumz  12134  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  ntrivcvgap  12293  prodmodclem2  12322  zproddc  12324  prod1dc  12331  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  nnmindc  12789  uzwodc  12792  pceu  13052  4sqlemafi  13152  4sqlem12  13159  ennnfone  13294  enctlem  13301  unct  13311  gzsumfzval  13688  sgrpidmndm  13710  gsumvalfi  14129  subrngintm  14493  subrgintm  14524  islssm  14666  lss0cl  14678  islidlm  14788  eltg3  15081  tgtop  15092  tgidm  15098  tgrest  15193  tgcn  15232  xblm  15441  dvfgg  15712  dvcnp2cntop  15723  2lgslem1  16124  pwtrufal  16941