Theorem exlimdv 1936

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2204. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1971, ax-7 2011. (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 1920	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1915	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  exlimdvv  1937  exlimddv  1938  ax13lem1  2373  ax13  2374  nfeqf  2380  axc15  2421  sssn  4828  elpreqprb  4867  reusv2lem2  5396  ralxfr2d  5407  euotd  5512  wefrc  5669  wereu2  5672  releldmb  5943  relelrnb  5944  iss  6033  frpomin  6338  onfr  6400  dffv2  6983  dff3  7098  elunirn  7246  fsnex  7277  f1prex  7278  isomin  7330  isofrlem  7333  ovmpt4g  7551  soex  7908  f1oweALT  7955  op1steq  8015  fo2ndf  8103  frxp3  8133  mpoxopynvov0g  8195  reldmtpos  8215  rntpos  8220  frrlem10  8276  fprresex  8291  wfrlem12OLD  8316  wfrlem17OLD  8321  erdisj  8751  map0g  8874  resixpfo  8926  domdifsn  9050  xpdom3  9066  domunsncan  9068  enfixsn  9077  sucdom2OLD  9078  fodomr  9124  mapdom2  9144  mapdom3  9145  rexdif1en  9154  pssnn  9164  ssfiALT  9170  domfi  9188  sucdom2  9202  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  0sdom1dom  9234  sdom1  9238  1sdom2dom  9243  pssnnOLD  9261  findcard2OLD  9280  ac6sfi  9283  isfinite2  9297  xpfiOLD  9314  domunfican  9316  fiint  9320  fodomfib  9322  mapfien2  9400  marypha1lem  9424  ordiso  9507  hartogslem1  9533  brwdom2  9564  wdomtr  9566  brwdom3  9573  unwdomg  9575  xpwdomg  9576  unxpwdom2  9579  inf3lem2  9620  ttrclss  9711  dmttrcl  9712  rnttrcl  9713  ttrclselem2  9717  epfrs  9722  tcmin  9732  frmin  9740  cplem1  9880  pm54.43  9992  dfac8alem  10020  dfac8b  10022  dfac8clem  10023  ac10ct  10025  acni2  10037  acndom  10042  numwdom  10050  wdomfil  10052  wdomnumr  10055  iunfictbso  10105  dfac2b  10121  dfac9  10127  kmlem13  10153  djuinf  10179  fictb  10236  cfeq0  10247  cff1  10249  cfflb  10250  cofsmo  10260  cfsmolem  10261  coftr  10264  infpssr  10299  fin4en1  10300  fin23lem7  10307  isf34lem4  10368  axcc3  10429  domtriomlem  10433  axdc2lem  10439  axdc3lem2  10442  axdc3lem4  10444  axdc4lem  10446  ac6num  10470  ttukeylem6  10505  ttukeyg  10508  fodomb  10517  iundom2g  10531  alephreg  10573  fpwwe2lem10  10631  fpwwe2lem11  10632  canthp1  10645  pwfseq  10655  gruen  10803  grudomon  10808  gruina  10809  grur1  10811  ltexnq  10966  ltbtwnnq  10969  genpn0  10994  psslinpr  11022  prlem934  11024  ltaddpr  11025  ltexprlem2  11028  ltexprlem6  11032  ltexprlem7  11033  reclem2pr  11039  reclem4pr  11041  suplem1pr  11043  negn0  11639  sup2  12166  supaddc  12177  supmul1  12179  zsupss  12917  fiinfnf1o  14306  hasheqf1oi  14307  hashfun  14393  hashf1  14414  rtrclreclem3  15003  rlimdm  15491  climcau  15613  caucvgb  15622  summolem2  15658  zsum  15660  sumz  15664  fsumf1o  15665  fsumss  15667  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumconst  15732  fsumrelem  15749  ntrivcvg  15839  prodmolem2  15875  zprod  15877  prod1  15884  fprodf1o  15886  fprodss  15888  fprodcl2lem  15890  fprodmul  15900  fproddiv  15901  fprodconst  15918  fprodn0  15919  ruclem13  16181  4sqlem12  16885  vdwapun  16903  vdwlem9  16918  vdwlem10  16919  ramz  16954  ramub1  16957  firest  17374  mremre  17544  isacs2  17593  iscatd2  17621  cicsym  17747  sscfn1  17760  sscfn2  17761  initoeu2  17962  gsumval2a  18600  symggen  19332  cyggex2  19759  gsumval3  19769  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  gsumzoppg  19806  gsum2d2  19836  pgpfac1lem5  19943  ablfaclem3  19951  lss0cl  20549  lspsnat  20750  cnsubrg  20997  gsumfsum  21004  obslbs  21276  lmiclbs  21383  lmisfree  21388  mdetdiaglem  22091  mdet0  22099  eltg3  22456  tgtop  22467  tgidm  22474  ppttop  22501  toponmre  22588  tgrest  22654  neitr  22675  tgcn  22747  cmpsublem  22894  cmpsub  22895  iunconnlem  22922  unconn  22924  1stcfb  22940  2ndcctbss  22950  2ndcdisj  22951  1stcelcls  22956  1stccnp  22957  locfincmp  23021  comppfsc  23027  1stckgen  23049  ptuni2  23071  ptbasfi  23076  ptpjopn  23107  ptclsg  23110  ptcnp  23117  prdstopn  23123  txindis  23129  txtube  23135  txcmplem1  23136  txcmplem2  23137  xkococnlem  23154  txconn  23184  trfbas2  23338  filtop  23350  filconn  23378  filssufilg  23406  fmfnfm  23453  ufldom  23457  hauspwpwf1  23482  alexsubALTlem3  23544  alexsubALT  23546  ptcmplem2  23548  tmdgsum2  23591  tgptsmscld  23646  ustfilxp  23708  xbln0  23911  opnreen  24338  metdsre  24360  cnheibor  24462  phtpc01  24503  cfilfcls  24782  cmetcaulem  24796  iscmet3  24801  ovolctb  24998  ovoliunlem3  25012  ovoliunnul  25015  ovolicc2lem5  25029  ovolicc2  25030  dyadmbl  25108  vitali  25121  itg11  25199  bddmulibl  25347  perfdvf  25411  dvcnp2  25428  dvlip  25501  dvne0  25519  fta1g  25676  fta1  25812  ulmcau  25898  pserulm  25925  wilthlem2  26562  dchrvmasumif  26995  rpvmasum2  27004  dchrisum0re  27005  dchrisum0lem3  27011  dchrisum0  27012  dchrmusum  27016  dchrvmasum  27017  noinfno  27210  nocvxmin  27269  sltlpss  27390  axcontlem10  28220  usgr1v0e  28572  wlkiswwlks  29119  wlkiswwlkupgr  29121  wlklnwwlkn  29127  wlklnwwlknupgr  29129  umgrwwlks2on  29200  elwwlks2  29209  elwspths2spth  29210  clwlkclwwlklem3  29243  clwlkclwwlkfo  29251  frgr3vlem2  29516  spansncvi  30892  2ndresdju  31861  fnpreimac  31883  qsidomlem2  32560  reff  32807  locfinreflem  32808  cmpcref  32818  fmcncfil  32899  volmeas  33217  omssubadd  33287  bnj849  33924  acycgrislfgr  34131  derangenlem  34150  cvmsss2  34253  cvmopnlem  34257  cvmfolem  34258  cvmliftmolem2  34261  cvmliftlem15  34277  cvmlift2lem10  34291  cvmlift3lem8  34305  satfdmlem  34347  sat1el2xp  34358  fmlasuc  34365  fundmpss  34726  gg-dvcnp2  35162  fnessref  35230  refssfne  35231  neibastop2lem  35233  neibastop2  35234  fnemeet2  35240  fnejoin2  35242  tailfb  35250  knoppcnlem9  35365  isinf2  36274  pibt2  36286  wl-ax13lem1  36363  wl-sbcom2d  36414  matunitlindflem2  36473  poimirlem25  36501  poimirlem27  36503  heicant  36511  itg2addnclem  36527  sdclem1  36599  fdc  36601  istotbnd3  36627  sstotbnd2  36630  prdsbnd2  36651  heibor1lem  36665  heiborlem1  36667  heiborlem10  36676  heibor  36677  riscer  36844  divrngidl  36884  iss2  37201  eqvreldisj  37472  disjlem17  37657  prtlem17  37734  ax12eq  37799  ax12el  37800  ax12inda  37806  ax12v2-o  37807  osumcllem8N  38822  pexmidlem5N  38833  mapdrvallem2  40504  sn-sup2  41338  onexomgt  41975  onexoegt  41978  omabs2  42067  clcnvlem  42359  onfrALT  43295  chordthmALT  43679  snelmap  43756  ssnnf1octb  43878  choicefi  43884  mapss2  43889  difmap  43891  axccdom  43906  infxrlesupxr  44132  inficc  44233  fsumnncl  44274  stoweidlem43  44745  stoweidlem48  44750  stoweidlem57  44759  stoweidlem60  44762  qndenserrnopn  45000  issalnnd  45047  subsaliuncl  45060  sge0cl  45083  nnfoctbdj  45158  ismeannd  45169  caragenunicl  45226  isomennd  45233  ovn0lem  45267  ovnsubaddlem2  45273  hspdifhsp  45318  hspmbllem3  45330  smflimlem6  45478  smfpimbor1lem1  45500  smfpimcc  45510  smfsuplem2  45514  rlimdmafv  45871  dfatcolem  45949  rlimdmafv2  45952  isomushgr  46480  isomuspgr  46488  isomgrsym  46490  isomgrtr  46493  mgmpropd  46531  c0snmgmhm  46698  opnneilv  47494  thincciso  47622