Theorem exlimdv 1952

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

Syntax hints:   → wi 4  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  exlimdvv  1953  exlimddv  1954  ax13lem1  2404  ax13  2405  nfeqf  2411  axc15  2452  sssn  4781  elpreqprb  4823  reusv2lem2  5353  ralxfr2d  5364  euotd  5479  wefrc  5637  wereu2  5640  releldmb  5918  relelrnb  5919  iss  6020  frpomin  6322  onfr  6380  dffv2  6957  dff3  7076  elunirn  7230  fsnex  7262  f1prex  7263  isomin  7316  isofrlem  7319  ovmpt4g  7538  soex  7897  f1oweALT  7948  op1steq  8009  fo2ndf  8094  frxp3  8125  mpoxopynvov0g  8188  reldmtpos  8208  rntpos  8213  frrlem10  8270  fprresex  8285  erdisj  8730  map0g  8860  resixpfo  8912  domdifsn  9026  xpdom3  9041  domunsncan  9043  enfixsn  9052  fodomr  9094  mapdom2  9114  mapdom3  9115  rexdif1en  9123  pssnn  9131  ssfiALT  9136  domfi  9151  sucdom2  9165  phplem2  9167  php3  9171  0sdom1dom  9184  sdom1  9188  1sdom2dom  9192  ac6sfi  9222  isfinite2  9236  domunfican  9260  fiint  9265  fodomfir  9266  fodomfib  9267  fodomfibOLD  9268  mapfien2  9349  marypha1lem  9373  ordiso  9458  hartogslem1  9484  brwdom2  9515  wdomtr  9517  brwdom3  9524  unwdomg  9526  xpwdomg  9527  unxpwdom2  9530  inf3lem2  9578  ttrclss  9669  dmttrcl  9670  rnttrcl  9671  ttrclselem2  9675  epfrs  9680  tcmin  9688  frmin  9701  cplem1  9841  pm54.43  9953  dfac8alem  9979  dfac8b  9981  dfac8clem  9982  ac10ct  9984  acni2  9996  acndom  10001  numwdom  10009  wdomfil  10011  wdomnumr  10014  iunfictbso  10064  dfac2b  10081  dfac9  10087  kmlem13  10113  djuinf  10139  fictb  10194  cfeq0  10207  cff1  10209  cfflb  10210  cofsmo  10220  cfsmolem  10221  coftr  10224  infpssr  10259  fin4en1  10260  fin23lem7  10267  isf34lem4  10328  axcc3  10389  domtriomlem  10393  axdc2lem  10399  axdc3lem2  10402  axdc3lem4  10404  axdc4lem  10406  ac6num  10430  ttukeylem6  10465  ttukeyg  10468  fodomb  10477  iundom2g  10491  alephreg  10534  fpwwe2lem10  10592  fpwwe2lem11  10593  canthp1  10606  pwfseq  10616  gruen  10764  grudomon  10769  gruina  10770  grur1  10772  ltexnq  10927  ltbtwnnq  10930  genpn0  10955  psslinpr  10983  prlem934  10985  ltaddpr  10986  ltexprlem2  10989  ltexprlem6  10993  ltexprlem7  10994  reclem2pr  11000  reclem4pr  11002  suplem1pr  11004  negn0  11610  sup2  12142  supaddc  12153  supmul1  12155  zsupss  12932  fiinfnf1o  14357  hasheqf1oi  14358  hashfun  14444  hashf1  14464  hash3tpexb  14501  rtrclreclem3  15067  rlimdm  15569  climcau  15689  caucvgb  15698  summolem2  15734  zsum  15736  sumz  15740  fsumf1o  15741  fsumss  15743  fsumcl2lem  15749  fsumadd  15758  fsummulc2  15802  fsumconst  15808  fsumrelem  15826  ntrivcvg  15918  prodmolem2  15956  zprod  15958  prod1  15965  fprodf1o  15967  fprodss  15969  fprodcl2lem  15971  fprodmul  15981  fproddiv  15982  fprodconst  15999  fprodn0  16000  ruclem13  16265  4sqlem12  16983  vdwapun  17001  vdwlem9  17016  vdwlem10  17017  ramz  17052  ramub1  17055  firest  17452  mremre  17623  isacs2  17676  iscatd2  17704  cicsym  17828  sscfn1  17841  sscfn2  17842  initoeu2  18040  mgmpropd  18676  gsumval2a  18710  symggen  19501  cyggex2  19928  gsumval3  19938  gsumzres  19940  gsumzcl2  19941  gsumzf1o  19943  gsumzaddlem  19952  gsumconst  19965  gsumzmhm  19968  gsumzoppg  19975  gsum2d2  20005  pgpfac1lem5  20112  ablfaclem3  20120  c0snmgmhm  20498  lss0cl  21002  lspsnat  21203  cnsubrg  21467  gsumfsum  21474  obslbs  21770  lmiclbs  21877  lmisfree  21882  mdetdiaglem  22646  mdet0  22654  eltg3  23010  tgtop  23021  tgidm  23028  ppttop  23055  toponmre  23141  tgrest  23207  neitr  23228  tgcn  23300  cmpsublem  23447  cmpsub  23448  iunconnlem  23475  unconn  23477  1stcfb  23493  2ndcctbss  23503  2ndcdisj  23504  1stcelcls  23509  1stccnp  23510  locfincmp  23574  comppfsc  23580  1stckgen  23602  ptuni2  23624  ptbasfi  23629  ptpjopn  23660  ptclsg  23663  ptcnp  23670  prdstopn  23676  txindis  23682  txtube  23688  txcmplem1  23689  txcmplem2  23690  xkococnlem  23707  txconn  23737  trfbas2  23891  filtop  23903  filconn  23931  filssufilg  23959  fmfnfm  24006  ufldom  24010  hauspwpwf1  24035  alexsubALTlem3  24097  alexsubALT  24099  ptcmplem2  24101  tmdgsum2  24144  tgptsmscld  24199  ustfilxp  24261  xbln0  24462  opnreen  24880  metdsre  24902  cnheibor  25005  phtpc01  25046  cfilfcls  25324  cmetcaulem  25338  iscmet3  25343  ovolctb  25540  ovoliunlem3  25554  ovoliunnul  25557  ovolicc2lem5  25571  ovolicc2  25572  dyadmbl  25650  vitali  25663  itg11  25741  bddmulibl  25889  perfdvf  25953  dvcnp2  25970  dvlip  26043  dvne0  26061  fta1g  26218  fta1  26360  ulmcau  26446  pserulm  26473  wilthlem2  27121  dchrvmasumif  27555  rpvmasum2  27564  dchrisum0re  27565  dchrisum0lem3  27571  dchrisum0  27572  dchrmusum  27576  dchrvmasum  27577  noinfno  27770  nobdaymin  27834  ltslpss  27989  axcontlem10  29131  usgr1v0e  29484  wlkiswwlks  30033  wlkiswwlkupgr  30035  wlklnwwlkn  30041  wlklnwwlknupgr  30043  usgrwwlks2on  30115  umgrwwlks2on  30116  elwwlks2  30126  elwspths2spth  30127  clwlkclwwlklem3  30160  clwlkclwwlkfo  30168  frgr3vlem2  30433  spansncvi  31812  2ndresdju  32812  fnpreimac  32833  gsumwrd2dccatlem  33218  qsidomlem2  33601  reff  34097  locfinreflem  34098  cmpcref  34108  fmcncfil  34189  volmeas  34489  omssubadd  34558  bnj849  35181  r1filimi  35360  onvfowev  35420  acycgrislfgr  35463  derangenlem  35482  cvmsss2  35585  cvmopnlem  35589  cvmfolem  35590  cvmliftmolem2  35593  cvmliftlem15  35609  cvmlift2lem10  35623  cvmlift3lem8  35637  satfdmlem  35679  sat1el2xp  35690  fmlasuc  35697  fundmpss  36078  fnessref  36678  refssfne  36679  neibastop2lem  36681  neibastop2  36682  fnemeet2  36688  fnejoin2  36690  tailfb  36698  axuntco  36800  dfttc4lem2  36850  knoppcnlem9  36900  isinf2  37860  pibt2  37872  wl-ax13lem1  37949  wl-sbcom2d  38025  matunitlindflem2  38077  poimirlem25  38105  poimirlem27  38107  heicant  38115  itg2addnclem  38131  sdclem1  38203  fdc  38205  istotbnd3  38231  sstotbnd2  38234  prdsbnd2  38255  heibor1lem  38269  heiborlem1  38271  heiborlem10  38280  heibor  38281  riscer  38448  divrngidl  38488  iss2  38804  eqvreldisj  39158  disjlem17  39362  prtlem17  39461  ax12eq  39526  ax12el  39527  ax12inda  39533  ax12v2-o  39534  osumcllem8N  40548  pexmidlem5N  40559  mapdrvallem2  42230  sn-sup2  43074  onexomgt  43779  onexoegt  43782  omabs2  43870  clcnvlem  44160  onfrALT  45086  chordthmALT  45469  relpmin  45489  relpfrlem  45490  modelaxreplem1  45515  wfac8prim  45539  snelmap  45623  ssnnf1octb  45733  choicefi  45738  mapss2  45743  difmap  45744  axccdom  45759  infxrlesupxr  45971  inficc  46071  fsumnncl  46109  stoweidlem43  46578  stoweidlem48  46583  stoweidlem57  46592  stoweidlem60  46595  qndenserrnopn  46833  issalnnd  46880  subsaliuncl  46893  sge0cl  46916  nnfoctbdj  46991  ismeannd  47002  caragenunicl  47059  isomennd  47066  ovn0lem  47100  ovnsubaddlem2  47106  hspdifhsp  47151  hspmbllem3  47163  smflimlem6  47311  smfpimbor1lem1  47333  smfpimcc  47343  smfsuplem2  47347  rlimdmafv  47732  dfatcolem  47810  rlimdmafv2  47813  grimuhgr  48470  grimcnv  48471  grimco  48472  uhgrimedgi  48473  isuspgrim0  48477  gricushgr  48500  gricsym  48504  uhgrimisgrgric  48514  clnbgrgrimlem  48516  clnbgrgrim  48517  grimedg  48518  grtriprop  48524  usgrgrtrirex  48533  isubgr3stgrlem3  48551  uspgrlim  48575  grlimprclnbgredg  48580  grlimgredgex  48583  grlimgrtri  48586  xpco2  49439  opnneilv  49491  thincciso  50035