Theorem exlimdv 1966

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exlimdvv  1967  exlimddv  1968  ax13lem1  2404  ax13  2405  nfeqf  2411  axc15  2452  sssn  4787  elpreqprb  4828  reusv2lem2  5361  ralxfr2d  5372  euotd  5486  wefrc  5645  wereu2  5648  releldmb  5928  relelrnb  5929  iss  6027  frpomin  6342  onfr  6401  dffv2  6978  dff3  7098  elunirn  7253  fsnex  7289  f1prex  7290  isomin  7343  isofrlem  7346  ovmpt4g  7565  soex  7931  f1oweALT  7982  op1steq  8043  fo2ndf  8130  frxp3  8161  mpoxopynvov0g  8224  reldmtpos  8244  rntpos  8249  frrlem10  8306  fprresex  8321  erdisj  8768  map0g  8905  resixpfo  8957  domdifsn  9072  xpdom3  9087  domunsncan  9089  enfixsn  9098  fodomr  9140  mapdom2  9160  mapdom3  9161  rexdif1en  9169  pssnn  9177  ssfiALT  9182  domfi  9197  sucdom2  9211  phplem2  9213  php3  9217  0sdom1dom  9230  sdom1  9234  1sdom2dom  9238  ac6sfi  9268  isfinite2  9283  domunfican  9306  fiint  9311  fodomfir  9312  fodomfib  9313  mapfien2  9394  marypha1lem  9418  ordiso  9503  hartogslem1  9529  brwdom2  9560  wdomtr  9562  brwdom3  9569  unwdomg  9571  xpwdomg  9572  unxpwdom2  9575  inf3lem2  9623  ttrclss  9714  dmttrcl  9715  rnttrcl  9716  ttrclselem2  9720  epfrs  9725  tcmin  9733  frmin  9746  r1filimi  9896  cplem1  9943  cplem1OLD  9944  karden  9952  pm54.43  10075  dfac8alem  10101  dfac8b  10103  dfac8clem  10104  ac10ct  10106  acni2  10118  acndom  10123  numwdom  10131  wdomfil  10133  wdomnumr  10136  iunfictbso  10186  dfac2b  10202  dfac9  10208  kmlem13  10234  djuinf  10260  fictb  10315  cfeq0  10327  cff1  10329  cfflb  10330  cofsmo  10340  cfsmolem  10341  coftr  10344  infpssr  10379  fin4en1  10380  fin23lem7  10387  isf34lem4  10448  axcc3  10509  domtriomlem  10513  axdc2lem  10519  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  ac6num  10550  ttukeylem6  10585  ttukeyg  10588  fodomb  10598  iundom2g  10617  alephreg  10660  fpwwe2lem10  10718  fpwwe2lem11  10719  canthp1  10732  pwfseq  10742  gruen  10890  grudomon  10895  gruina  10896  grur1  10898  ltexnq  11053  ltbtwnnq  11056  genpn0  11081  psslinpr  11109  prlem934  11111  ltaddpr  11112  ltexprlem2  11115  ltexprlem6  11119  ltexprlem7  11120  reclem2pr  11126  reclem4pr  11128  suplem1pr  11130  negn0  11738  sup2  12266  supaddc  12277  supmul1  12279  zsupss  13057  fiinfnf1o  14487  hasheqf1oi  14488  hashfun  14575  hashf1  14595  hash3tpexb  14632  rtrclreclem3  15206  rlimdm  15711  climcau  15831  caucvgb  15840  summolem2  15875  zsum  15877  sumz  15881  fsumf1o  15882  fsumss  15884  fsumcl2lem  15890  fsumadd  15899  fsummulc2  15943  fsumconst  15949  fsumrelem  15967  ntrivcvg  16059  prodmolem2  16095  zprod  16097  prod1  16104  fprodf1o  16106  fprodss  16108  fprodcl2lem  16110  fprodmul  16120  fproddiv  16121  fprodconst  16138  fprodn0  16139  ruclem13  16403  4sqlem12  17127  vdwapun  17145  vdwlem9  17160  vdwlem10  17161  ramz  17196  ramub1  17199  firest  17596  mremre  17767  isacs2  17820  iscatd2  17848  cicsym  17972  sscfn1  17985  sscfn2  17986  initoeu2  18184  mgmpropd  18822  gsumval2a  18867  symggen  19677  cyggex2  20104  gsumval3  20114  gsumzres  20116  gsumzcl2  20117  gsumzf1o  20119  gsumzaddlem  20128  gsumconst  20141  gsumzmhm  20144  gsumzoppg  20151  gsum2d2  20181  pgpfac1lem5  20288  ablfaclem3  20296  c0snmgmhm  20685  lss0cl  21215  lspsnat  21416  qsidomlem2  21630  cnsubrg  21726  gsumfsum  21733  obslbs  22029  lmiclbs  22136  lmisfree  22141  mdetdiaglem  22906  mdet0  22914  matunitlindflem2  22988  eltg3  23273  tgtop  23284  tgidm  23291  ppttop  23318  toponmre  23404  tgrest  23470  neitr  23491  tgcn  23563  cmpsublem  23710  cmpsub  23711  iunconnlem  23738  unconn  23740  1stcfb  23756  2ndcctbss  23767  2ndcdisj  23768  1stcelcls  23773  1stccnp  23774  locfincmp  23838  comppfsc  23844  1stckgen  23866  ptuni2  23888  ptbasfi  23893  ptpjopn  23924  ptclsg  23927  ptcnp  23934  prdstopn  23940  txindis  23946  txtube  23952  txcmplem1  23953  txcmplem2  23954  xkococnlem  23971  txconn  24001  trfbas2  24155  filtop  24167  filconn  24195  filssufilg  24223  fmfnfm  24270  ufldom  24274  hauspwpwf1  24299  alexsubALTlem3  24361  alexsubALT  24363  ptcmplem2  24365  tmdgsum2  24408  tgptsmscld  24463  ustfilxp  24525  xbln0  24726  opnreen  25144  metdsre  25166  cnheibor  25269  phtpc01  25310  cfilfcls  25588  cmetcaulem  25602  iscmet3  25607  ovolctb  25804  ovoliunlem3  25818  ovoliunnul  25821  ovolicc2lem5  25835  ovolicc2  25836  dyadmbl  25914  vitali  25927  itg11  26005  bddmulibl  26152  perfdvf  26216  dvcnp2  26233  dvlip  26306  dvne0  26324  fta1g  26481  fta1  26622  ulmcau  26715  pserulm  26742  wilthlem2  27389  dchrvmasumif  27823  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem3  27839  dchrisum0  27840  dchrmusum  27844  dchrvmasum  27845  noinfno  28068  nobdaymin  28132  ltslpss  28287  axcontlem10  29544  usgr1v0e  29900  wlkiswwlks  30458  wlkiswwlkupgr  30460  wlklnwwlkn  30466  wlklnwwlknupgr  30468  usgrwwlks2on  30540  umgrwwlks2on  30541  elwwlks2  30551  elwspths2spth  30552  clwlkclwwlklem3  30585  clwlkclwwlkfo  30593  frgr3vlem2  30868  spansncvi  32247  2ndresdju  33236  fnpreimac  33257  gsumwrd2dccatlem  33631  reff  34464  locfinreflem  34465  cmpcref  34475  fmcncfil  34556  volmeas  34857  omssubadd  34925  bnj849  35548  kardfi  35821  onvfowev  35878  acycgrislfgr  35896  derangenlem  35915  cvmsss2  36018  cvmopnlem  36022  cvmfolem  36023  cvmliftmolem2  36026  cvmliftlem15  36042  cvmlift2lem10  36056  cvmlift3lem8  36070  satfdmlem  36112  sat1el2xp  36123  fmlasuc  36130  fundmpss  36511  fnessref  37125  refssfne  37126  neibastop2lem  37128  neibastop2  37129  fnemeet2  37135  fnejoin2  37137  tailfb  37145  axuntco  37247  dfttc4lem2  37297  knoppcnlem9  37347  isinf2  38308  pibt2  38320  wl-ax13lem1  38397  wl-sbcom2d  38473  poimirlem25  38543  poimirlem27  38545  heicant  38553  itg2addnclem  38569  sdclem1  38657  fdc  38659  istotbnd3  38685  sstotbnd2  38688  prdsbnd2  38709  heibor1lem  38723  heiborlem1  38725  heiborlem10  38734  heibor  38735  riscer  38902  divrngidl  38942  iss2  39256  eqvreldisj  39610  disjlem17  39814  prtlem17  39913  ax12eq  39978  ax12el  39979  ax12inda  39985  ax12v2-o  39986  osumcllem8N  41000  pexmidlem5N  41011  mapdrvallem2  42682  sn-sup2  43535  onexomgt  44227  onexoegt  44230  omabs2  44318  clcnvlem  44608  onfrALT  45517  chordthmALT  45900  relpmin  45920  relpfrlem  45921  modelaxreplem1  45946  wfac8prim  45970  snelmap  46068  ssnnf1octb  46178  choicefi  46183  mapss2  46188  difmap  46189  axccdom  46204  infxrlesupxr  46415  inficc  46515  fsumnncl  46553  stoweidlem43  47022  stoweidlem48  47027  stoweidlem57  47036  stoweidlem60  47039  qndenserrnopn  47277  issalnnd  47324  subsaliuncl  47337  sge0cl  47360  nnfoctbdj  47435  ismeannd  47446  caragenunicl  47503  isomennd  47510  ovn0lem  47544  ovnsubaddlem2  47550  hspdifhsp  47595  hspmbllem3  47607  smflimlem6  47755  smfpimbor1lem1  47777  smfpimcc  47787  smfsuplem2  47791  rlimdmafv  48216  dfatcolem  48294  rlimdmafv2  48297  grimuhgr  48954  grimcnv  48955  grimco  48956  uhgrimedgi  48957  isuspgrim0  48961  gricushgr  48984  gricsym  48988  uhgrimisgrgric  48998  clnbgrgrimlem  49000  clnbgrgrim  49001  grimedg  49002  grtriprop  49008  usgrgrtrirex  49017  isubgr3stgrlem3  49035  uspgrlim  49059  grlimprclnbgredg  49064  grlimgredgex  49067  grlimgrtri  49070  xpco2  49936  opnneilv  49986  thincciso  50530