Theorem exlimdv 1937

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

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

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

This theorem is referenced by:  exlimdvv  1938  exlimddv  1939  ax13lem1  2374  ax13  2375  nfeqf  2381  axc15  2422  sssn  4756  elpreqprb  4795  reusv2lem2  5317  ralxfr2d  5328  euotd  5421  wefrc  5574  wereu2  5577  releldmb  5844  relelrnb  5845  iss  5932  frpomin  6228  onfr  6290  dffv2  6845  dff3  6958  elunirn  7106  fsnex  7135  f1prex  7136  isomin  7188  isofrlem  7191  ovmpt4g  7398  soex  7742  f1oweALT  7788  op1steq  7848  fo2ndf  7933  mpoxopynvov0g  8001  reldmtpos  8021  rntpos  8026  frrlem10  8082  fprresex  8097  wfrlem12OLD  8122  wfrlem17OLD  8127  erdisj  8508  map0g  8630  resixpfo  8682  domdifsn  8795  xpdom3  8810  domunsncan  8812  enfixsn  8821  sucdom2  8822  fodomr  8864  mapdom2  8884  mapdom3  8885  phplem4  8895  php3  8899  pssnn  8913  ssfiALT  8919  domfi  8935  pssnnOLD  8969  findcard2OLD  8986  ac6sfi  8988  isfinite2  9002  xpfi  9015  domunfican  9017  fiint  9021  fodomfib  9023  mapfien2  9098  marypha1lem  9122  ordiso  9205  hartogslem1  9231  brwdom2  9262  wdomtr  9264  brwdom3  9271  unwdomg  9273  xpwdomg  9274  unxpwdom2  9277  inf3lem2  9317  epfrs  9420  tcmin  9430  frmin  9438  cplem1  9578  pm54.43  9690  dfac8alem  9716  dfac8b  9718  dfac8clem  9719  ac10ct  9721  acni2  9733  acndom  9738  numwdom  9746  wdomfil  9748  wdomnumr  9751  iunfictbso  9801  dfac2b  9817  dfac9  9823  kmlem13  9849  djuinf  9875  fictb  9932  cfeq0  9943  cff1  9945  cfflb  9946  cofsmo  9956  cfsmolem  9957  coftr  9960  infpssr  9995  fin4en1  9996  fin23lem7  10003  isf34lem4  10064  axcc3  10125  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  ac6num  10166  ttukeylem6  10201  ttukeyg  10204  fodomb  10213  iundom2g  10227  alephreg  10269  fpwwe2lem10  10327  fpwwe2lem11  10328  canthp1  10341  pwfseq  10351  gruen  10499  grudomon  10504  gruina  10505  grur1  10507  ltexnq  10662  ltbtwnnq  10665  genpn0  10690  psslinpr  10718  prlem934  10720  ltaddpr  10721  ltexprlem2  10724  ltexprlem6  10728  ltexprlem7  10729  reclem2pr  10735  reclem4pr  10737  suplem1pr  10739  negn0  11334  sup2  11861  supaddc  11872  supmul1  11874  zsupss  12606  fiinfnf1o  13992  hasheqf1oi  13994  hashfun  14080  hashf1  14099  rtrclreclem3  14699  rlimdm  15188  climcau  15310  caucvgb  15319  summolem2  15356  zsum  15358  sumz  15362  fsumf1o  15363  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  fsummulc2  15424  fsumconst  15430  fsumrelem  15447  ntrivcvg  15537  prodmolem2  15573  zprod  15575  prod1  15582  fprodf1o  15584  fprodss  15586  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodconst  15616  fprodn0  15617  ruclem13  15879  4sqlem12  16585  vdwapun  16603  vdwlem9  16618  vdwlem10  16619  ramz  16654  ramub1  16657  firest  17060  mremre  17230  isacs2  17279  iscatd2  17307  cicsym  17433  sscfn1  17446  sscfn2  17447  initoeu2  17647  gsumval2a  18284  symggen  18993  cyggex2  19413  gsumval3  19423  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  gsum2d2  19490  pgpfac1lem5  19597  ablfaclem3  19605  lss0cl  20123  lspsnat  20322  cnsubrg  20570  gsumfsum  20577  obslbs  20847  lmiclbs  20954  lmisfree  20959  mdetdiaglem  21655  mdet0  21663  eltg3  22020  tgtop  22031  tgidm  22038  ppttop  22065  toponmre  22152  tgrest  22218  neitr  22239  tgcn  22311  cmpsublem  22458  cmpsub  22459  iunconnlem  22486  unconn  22488  1stcfb  22504  2ndcctbss  22514  2ndcdisj  22515  1stcelcls  22520  1stccnp  22521  locfincmp  22585  comppfsc  22591  1stckgen  22613  ptuni2  22635  ptbasfi  22640  ptpjopn  22671  ptclsg  22674  ptcnp  22681  prdstopn  22687  txindis  22693  txtube  22699  txcmplem1  22700  txcmplem2  22701  xkococnlem  22718  txconn  22748  trfbas2  22902  filtop  22914  filconn  22942  filssufilg  22970  fmfnfm  23017  ufldom  23021  hauspwpwf1  23046  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem2  23112  tmdgsum2  23155  tgptsmscld  23210  ustfilxp  23272  xbln0  23475  opnreen  23900  metdsre  23922  cnheibor  24024  phtpc01  24065  cfilfcls  24343  cmetcaulem  24357  iscmet3  24362  ovolctb  24559  ovoliunlem3  24573  ovoliunnul  24576  ovolicc2lem5  24590  ovolicc2  24591  dyadmbl  24669  vitali  24682  itg11  24760  bddmulibl  24908  perfdvf  24972  dvcnp2  24989  dvlip  25062  dvne0  25080  fta1g  25237  fta1  25373  ulmcau  25459  pserulm  25486  wilthlem2  26123  dchrvmasumif  26556  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem3  26572  dchrisum0  26573  dchrmusum  26577  dchrvmasum  26578  axcontlem10  27244  usgr1v0e  27596  wlkiswwlks  28142  wlkiswwlkupgr  28144  wlklnwwlkn  28150  wlklnwwlknupgr  28152  umgrwwlks2on  28223  elwwlks2  28232  elwspths2spth  28233  clwlkclwwlklem3  28266  clwlkclwwlkfo  28274  frgr3vlem2  28539  spansncvi  29915  2ndresdju  30887  fnpreimac  30910  qsidomlem2  31531  reff  31691  locfinreflem  31692  cmpcref  31702  fmcncfil  31783  volmeas  32099  omssubadd  32167  bnj849  32805  acycgrislfgr  33014  derangenlem  33033  cvmsss2  33136  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem2  33144  cvmliftlem15  33160  cvmlift2lem10  33174  cvmlift3lem8  33188  satfdmlem  33230  sat1el2xp  33241  fmlasuc  33248  fundmpss  33646  ttrclss  33706  dmttrcl  33707  rnttrcl  33708  ttrclselem2  33712  frxp3  33724  noinfno  33848  nocvxmin  33900  sltlpss  34014  fnessref  34473  refssfne  34474  neibastop2lem  34476  neibastop2  34477  fnemeet2  34483  fnejoin2  34485  tailfb  34493  knoppcnlem9  34608  isinf2  35503  pibt2  35515  wl-ax13lem1  35592  wl-sbcom2d  35643  matunitlindflem2  35701  poimirlem25  35729  poimirlem27  35731  heicant  35739  itg2addnclem  35755  sdclem1  35828  fdc  35830  istotbnd3  35856  sstotbnd2  35859  prdsbnd2  35880  heibor1lem  35894  heiborlem1  35896  heiborlem10  35905  heibor  35906  riscer  36073  divrngidl  36113  iss2  36406  eqvreldisj  36654  prtlem17  36817  ax12eq  36882  ax12el  36883  ax12inda  36889  ax12v2-o  36890  osumcllem8N  37904  pexmidlem5N  37915  mapdrvallem2  39586  sn-sup2  40360  clcnvlem  41120  onfrALT  42058  chordthmALT  42442  snelmap  42521  ssnnf1octb  42622  choicefi  42629  mapss2  42634  difmap  42636  axccdom  42651  infxrlesupxr  42866  inficc  42962  fsumnncl  43003  stoweidlem43  43474  stoweidlem48  43479  stoweidlem57  43488  stoweidlem60  43491  qndenserrnopn  43729  issalnnd  43774  subsaliuncl  43787  sge0cl  43809  nnfoctbdj  43884  ismeannd  43895  caragenunicl  43952  isomennd  43959  ovn0lem  43993  ovnsubaddlem2  43999  hspdifhsp  44044  hspmbllem3  44056  smflimlem6  44198  smfpimbor1lem1  44219  smfpimcc  44228  smfsuplem2  44232  rlimdmafv  44556  dfatcolem  44634  rlimdmafv2  44637  isomushgr  45166  isomuspgr  45174  isomgrsym  45176  isomgrtr  45179  mgmpropd  45217  c0snmgmhm  45360  opnneilv  46090  thincciso  46218