Theorem exlimdv 1933

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2212. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1967, ax-7 2008. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		exlimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	eximdv 1917	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1912	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  exlimdvv  1934  exlimddv  1935  ax13lem1  2372  ax13  2373  nfeqf  2379  axc15  2420  sssn  4780  elpreqprb  4822  reusv2lem2  5341  ralxfr2d  5352  euotd  5460  wefrc  5617  wereu2  5620  releldmb  5892  relelrnb  5893  iss  5990  frpomin  6292  onfr  6350  dffv2  6922  dff3  7038  elunirn  7191  fsnex  7224  f1prex  7225  isomin  7278  isofrlem  7281  ovmpt4g  7500  soex  7861  f1oweALT  7914  op1steq  7975  fo2ndf  8061  frxp3  8091  mpoxopynvov0g  8154  reldmtpos  8174  rntpos  8179  frrlem10  8235  fprresex  8250  erdisj  8689  map0g  8818  resixpfo  8870  domdifsn  8984  xpdom3  8999  domunsncan  9001  enfixsn  9010  fodomr  9052  mapdom2  9072  mapdom3  9073  rexdif1en  9082  pssnn  9092  ssfiALT  9098  domfi  9113  sucdom2  9127  phplem2  9129  php3  9133  0sdom1dom  9145  sdom1  9149  1sdom2dom  9153  ac6sfi  9189  isfinite2  9203  xpfiOLD  9228  domunfican  9230  fiint  9235  fiintOLD  9236  fodomfir  9237  fodomfib  9238  fodomfibOLD  9240  mapfien2  9318  marypha1lem  9342  ordiso  9427  hartogslem1  9453  brwdom2  9484  wdomtr  9486  brwdom3  9493  unwdomg  9495  xpwdomg  9496  unxpwdom2  9499  inf3lem2  9544  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  epfrs  9646  tcmin  9656  frmin  9664  cplem1  9804  pm54.43  9916  dfac8alem  9942  dfac8b  9944  dfac8clem  9945  ac10ct  9947  acni2  9959  acndom  9964  numwdom  9972  wdomfil  9974  wdomnumr  9977  iunfictbso  10027  dfac2b  10044  dfac9  10050  kmlem13  10076  djuinf  10102  fictb  10157  cfeq0  10169  cff1  10171  cfflb  10172  cofsmo  10182  cfsmolem  10183  coftr  10186  infpssr  10221  fin4en1  10222  fin23lem7  10229  isf34lem4  10290  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ac6num  10392  ttukeylem6  10427  ttukeyg  10430  fodomb  10439  iundom2g  10453  alephreg  10495  fpwwe2lem10  10553  fpwwe2lem11  10554  canthp1  10567  pwfseq  10577  gruen  10725  grudomon  10730  gruina  10731  grur1  10733  ltexnq  10888  ltbtwnnq  10891  genpn0  10916  psslinpr  10944  prlem934  10946  ltaddpr  10947  ltexprlem2  10950  ltexprlem6  10954  ltexprlem7  10955  reclem2pr  10961  reclem4pr  10963  suplem1pr  10965  negn0  11567  sup2  12099  supaddc  12110  supmul1  12112  zsupss  12856  fiinfnf1o  14275  hasheqf1oi  14276  hashfun  14362  hashf1  14382  hash3tpexb  14419  rtrclreclem3  14985  rlimdm  15476  climcau  15596  caucvgb  15605  summolem2  15641  zsum  15643  sumz  15647  fsumf1o  15648  fsumss  15650  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumconst  15715  fsumrelem  15732  ntrivcvg  15822  prodmolem2  15860  zprod  15862  prod1  15869  fprodf1o  15871  fprodss  15873  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodconst  15903  fprodn0  15904  ruclem13  16169  4sqlem12  16886  vdwapun  16904  vdwlem9  16919  vdwlem10  16920  ramz  16955  ramub1  16958  firest  17354  mremre  17524  isacs2  17577  iscatd2  17605  cicsym  17729  sscfn1  17742  sscfn2  17743  initoeu2  17941  mgmpropd  18543  gsumval2a  18577  symggen  19367  cyggex2  19794  gsumval3  19804  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumconst  19831  gsumzmhm  19834  gsumzoppg  19841  gsum2d2  19871  pgpfac1lem5  19978  ablfaclem3  19986  c0snmgmhm  20365  lss0cl  20868  lspsnat  21070  cnsubrg  21352  gsumfsum  21359  obslbs  21655  lmiclbs  21762  lmisfree  21767  mdetdiaglem  22501  mdet0  22509  eltg3  22865  tgtop  22876  tgidm  22883  ppttop  22910  toponmre  22996  tgrest  23062  neitr  23083  tgcn  23155  cmpsublem  23302  cmpsub  23303  iunconnlem  23330  unconn  23332  1stcfb  23348  2ndcctbss  23358  2ndcdisj  23359  1stcelcls  23364  1stccnp  23365  locfincmp  23429  comppfsc  23435  1stckgen  23457  ptuni2  23479  ptbasfi  23484  ptpjopn  23515  ptclsg  23518  ptcnp  23525  prdstopn  23531  txindis  23537  txtube  23543  txcmplem1  23544  txcmplem2  23545  xkococnlem  23562  txconn  23592  trfbas2  23746  filtop  23758  filconn  23786  filssufilg  23814  fmfnfm  23861  ufldom  23865  hauspwpwf1  23890  alexsubALTlem3  23952  alexsubALT  23954  ptcmplem2  23956  tmdgsum2  23999  tgptsmscld  24054  ustfilxp  24116  xbln0  24318  opnreen  24736  metdsre  24758  cnheibor  24870  phtpc01  24911  cfilfcls  25190  cmetcaulem  25204  iscmet3  25209  ovolctb  25407  ovoliunlem3  25421  ovoliunnul  25424  ovolicc2lem5  25438  ovolicc2  25439  dyadmbl  25517  vitali  25530  itg11  25608  bddmulibl  25756  perfdvf  25820  dvcnp2  25837  dvcnp2OLD  25838  dvlip  25914  dvne0  25932  fta1g  26091  fta1  26232  ulmcau  26320  pserulm  26347  wilthlem2  26995  dchrvmasumif  27430  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  dchrmusum  27451  dchrvmasum  27452  noinfno  27646  nobdaymin  27705  sltlpss  27840  axcontlem10  28936  usgr1v0e  29289  wlkiswwlks  29839  wlkiswwlkupgr  29841  wlklnwwlkn  29847  wlklnwwlknupgr  29849  umgrwwlks2on  29920  elwwlks2  29929  elwspths2spth  29930  clwlkclwwlklem3  29963  clwlkclwwlkfo  29971  frgr3vlem2  30236  spansncvi  31614  2ndresdju  32606  fnpreimac  32628  gsumwrd2dccatlem  33032  qsidomlem2  33403  reff  33808  locfinreflem  33809  cmpcref  33819  fmcncfil  33900  volmeas  34200  omssubadd  34270  bnj849  34894  acycgrislfgr  35127  derangenlem  35146  cvmsss2  35249  cvmopnlem  35253  cvmfolem  35254  cvmliftmolem2  35257  cvmliftlem15  35273  cvmlift2lem10  35287  cvmlift3lem8  35301  satfdmlem  35343  sat1el2xp  35354  fmlasuc  35361  fundmpss  35742  fnessref  36333  refssfne  36334  neibastop2lem  36336  neibastop2  36337  fnemeet2  36343  fnejoin2  36345  tailfb  36353  knoppcnlem9  36477  isinf2  37381  pibt2  37393  wl-ax13lem1  37470  wl-sbcom2d  37537  matunitlindflem2  37599  poimirlem25  37627  poimirlem27  37629  heicant  37637  itg2addnclem  37653  sdclem1  37725  fdc  37727  istotbnd3  37753  sstotbnd2  37756  prdsbnd2  37777  heibor1lem  37791  heiborlem1  37793  heiborlem10  37802  heibor  37803  riscer  37970  divrngidl  38010  iss2  38314  eqvreldisj  38593  disjlem17  38779  prtlem17  38857  ax12eq  38922  ax12el  38923  ax12inda  38929  ax12v2-o  38930  osumcllem8N  39945  pexmidlem5N  39956  mapdrvallem2  41627  sn-sup2  42467  onexomgt  43217  onexoegt  43220  omabs2  43308  clcnvlem  43599  onfrALT  44526  chordthmALT  44909  relpmin  44929  relpfrlem  44930  modelaxreplem1  44955  wfac8prim  44979  snelmap  45063  ssnnf1octb  45175  choicefi  45181  mapss2  45186  difmap  45188  axccdom  45203  infxrlesupxr  45419  inficc  45519  fsumnncl  45557  stoweidlem43  46028  stoweidlem48  46033  stoweidlem57  46042  stoweidlem60  46045  qndenserrnopn  46283  issalnnd  46330  subsaliuncl  46343  sge0cl  46366  nnfoctbdj  46441  ismeannd  46452  caragenunicl  46509  isomennd  46516  ovn0lem  46550  ovnsubaddlem2  46556  hspdifhsp  46601  hspmbllem3  46613  smflimlem6  46761  smfpimbor1lem1  46783  smfpimcc  46793  smfsuplem2  46797  rlimdmafv  47165  dfatcolem  47243  rlimdmafv2  47246  grimuhgr  47875  grimcnv  47876  grimco  47877  uhgrimedgi  47878  isuspgrim0  47882  gricushgr  47905  gricsym  47909  uhgrimisgrgric  47919  clnbgrgrimlem  47921  clnbgrgrim  47922  grimedg  47923  grtriprop  47929  usgrgrtrirex  47938  isubgr3stgrlem3  47956  uspgrlim  47980  grlimprclnbgredg  47985  grlimgredgex  47988  grlimgrtri  47991  xpco2  48845  opnneilv  48897  thincciso  49442