Theorem exlimdv 1934

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  exlimdvv  1935  exlimddv  1936  ax13lem1  2376  ax13  2377  nfeqf  2383  axc15  2424  sssn  4779  elpreqprb  4821  reusv2lem2  5341  ralxfr2d  5352  euotd  5458  wefrc  5615  wereu2  5618  releldmb  5892  relelrnb  5893  iss  5991  frpomin  6295  onfr  6353  dffv2  6926  dff3  7042  elunirn  7194  fsnex  7226  f1prex  7227  isomin  7280  isofrlem  7283  ovmpt4g  7502  soex  7860  f1oweALT  7913  op1steq  7974  fo2ndf  8060  frxp3  8090  mpoxopynvov0g  8153  reldmtpos  8173  rntpos  8178  frrlem10  8234  fprresex  8249  erdisj  8688  map0g  8818  resixpfo  8870  domdifsn  8984  xpdom3  8999  domunsncan  9001  enfixsn  9010  fodomr  9052  mapdom2  9072  mapdom3  9073  rexdif1en  9081  pssnn  9089  ssfiALT  9094  domfi  9109  sucdom2  9123  phplem2  9125  php3  9129  0sdom1dom  9141  sdom1  9145  1sdom2dom  9149  ac6sfi  9179  isfinite2  9193  domunfican  9217  fiint  9222  fodomfir  9223  fodomfib  9224  fodomfibOLD  9226  mapfien2  9304  marypha1lem  9328  ordiso  9413  hartogslem1  9439  brwdom2  9470  wdomtr  9472  brwdom3  9479  unwdomg  9481  xpwdomg  9482  unxpwdom2  9485  inf3lem2  9530  ttrclss  9621  dmttrcl  9622  rnttrcl  9623  ttrclselem2  9627  epfrs  9632  tcmin  9640  frmin  9653  cplem1  9793  pm54.43  9905  dfac8alem  9931  dfac8b  9933  dfac8clem  9934  ac10ct  9936  acni2  9948  acndom  9953  numwdom  9961  wdomfil  9963  wdomnumr  9966  iunfictbso  10016  dfac2b  10033  dfac9  10039  kmlem13  10065  djuinf  10091  fictb  10146  cfeq0  10158  cff1  10160  cfflb  10161  cofsmo  10171  cfsmolem  10172  coftr  10175  infpssr  10210  fin4en1  10211  fin23lem7  10218  isf34lem4  10279  axcc3  10340  domtriomlem  10344  axdc2lem  10350  axdc3lem2  10353  axdc3lem4  10355  axdc4lem  10357  ac6num  10381  ttukeylem6  10416  ttukeyg  10419  fodomb  10428  iundom2g  10442  alephreg  10484  fpwwe2lem10  10542  fpwwe2lem11  10543  canthp1  10556  pwfseq  10566  gruen  10714  grudomon  10719  gruina  10720  grur1  10722  ltexnq  10877  ltbtwnnq  10880  genpn0  10905  psslinpr  10933  prlem934  10935  ltaddpr  10936  ltexprlem2  10939  ltexprlem6  10943  ltexprlem7  10944  reclem2pr  10950  reclem4pr  10952  suplem1pr  10954  negn0  11557  sup2  12089  supaddc  12100  supmul1  12102  zsupss  12841  fiinfnf1o  14264  hasheqf1oi  14265  hashfun  14351  hashf1  14371  hash3tpexb  14408  rtrclreclem3  14974  rlimdm  15465  climcau  15585  caucvgb  15594  summolem2  15630  zsum  15632  sumz  15636  fsumf1o  15637  fsumss  15639  fsumcl2lem  15645  fsumadd  15654  fsummulc2  15698  fsumconst  15704  fsumrelem  15721  ntrivcvg  15811  prodmolem2  15849  zprod  15851  prod1  15858  fprodf1o  15860  fprodss  15862  fprodcl2lem  15864  fprodmul  15874  fproddiv  15875  fprodconst  15892  fprodn0  15893  ruclem13  16158  4sqlem12  16875  vdwapun  16893  vdwlem9  16908  vdwlem10  16909  ramz  16944  ramub1  16947  firest  17343  mremre  17514  isacs2  17567  iscatd2  17595  cicsym  17719  sscfn1  17732  sscfn2  17733  initoeu2  17931  mgmpropd  18567  gsumval2a  18601  symggen  19390  cyggex2  19817  gsumval3  19827  gsumzres  19829  gsumzcl2  19830  gsumzf1o  19832  gsumzaddlem  19841  gsumconst  19854  gsumzmhm  19857  gsumzoppg  19864  gsum2d2  19894  pgpfac1lem5  20001  ablfaclem3  20009  c0snmgmhm  20389  lss0cl  20889  lspsnat  21091  cnsubrg  21373  gsumfsum  21380  obslbs  21676  lmiclbs  21783  lmisfree  21788  mdetdiaglem  22533  mdet0  22541  eltg3  22897  tgtop  22908  tgidm  22915  ppttop  22942  toponmre  23028  tgrest  23094  neitr  23115  tgcn  23187  cmpsublem  23334  cmpsub  23335  iunconnlem  23362  unconn  23364  1stcfb  23380  2ndcctbss  23390  2ndcdisj  23391  1stcelcls  23396  1stccnp  23397  locfincmp  23461  comppfsc  23467  1stckgen  23489  ptuni2  23511  ptbasfi  23516  ptpjopn  23547  ptclsg  23550  ptcnp  23557  prdstopn  23563  txindis  23569  txtube  23575  txcmplem1  23576  txcmplem2  23577  xkococnlem  23594  txconn  23624  trfbas2  23778  filtop  23790  filconn  23818  filssufilg  23846  fmfnfm  23893  ufldom  23897  hauspwpwf1  23922  alexsubALTlem3  23984  alexsubALT  23986  ptcmplem2  23988  tmdgsum2  24031  tgptsmscld  24086  ustfilxp  24148  xbln0  24349  opnreen  24767  metdsre  24789  cnheibor  24901  phtpc01  24942  cfilfcls  25221  cmetcaulem  25235  iscmet3  25240  ovolctb  25438  ovoliunlem3  25452  ovoliunnul  25455  ovolicc2lem5  25469  ovolicc2  25470  dyadmbl  25548  vitali  25561  itg11  25639  bddmulibl  25787  perfdvf  25851  dvcnp2  25868  dvcnp2OLD  25869  dvlip  25945  dvne0  25963  fta1g  26122  fta1  26263  ulmcau  26351  pserulm  26378  wilthlem2  27026  dchrvmasumif  27461  rpvmasum2  27470  dchrisum0re  27471  dchrisum0lem3  27477  dchrisum0  27478  dchrmusum  27482  dchrvmasum  27483  noinfno  27677  nobdaymin  27736  sltlpss  27873  axcontlem10  28972  usgr1v0e  29325  wlkiswwlks  29875  wlkiswwlkupgr  29877  wlklnwwlkn  29883  wlklnwwlknupgr  29885  usgrwwlks2on  29957  umgrwwlks2on  29958  elwwlks2  29968  elwspths2spth  29969  clwlkclwwlklem3  30002  clwlkclwwlkfo  30010  frgr3vlem2  30275  spansncvi  31653  2ndresdju  32653  fnpreimac  32675  gsumwrd2dccatlem  33087  qsidomlem2  33462  reff  33924  locfinreflem  33925  cmpcref  33935  fmcncfil  34016  volmeas  34316  omssubadd  34385  bnj849  35009  r1filimi  35186  acycgrislfgr  35268  derangenlem  35287  cvmsss2  35390  cvmopnlem  35394  cvmfolem  35395  cvmliftmolem2  35398  cvmliftlem15  35414  cvmlift2lem10  35428  cvmlift3lem8  35442  satfdmlem  35484  sat1el2xp  35495  fmlasuc  35502  fundmpss  35883  fnessref  36473  refssfne  36474  neibastop2lem  36476  neibastop2  36477  fnemeet2  36483  fnejoin2  36485  tailfb  36493  knoppcnlem9  36617  isinf2  37522  pibt2  37534  wl-ax13lem1  37611  wl-sbcom2d  37678  matunitlindflem2  37730  poimirlem25  37758  poimirlem27  37760  heicant  37768  itg2addnclem  37784  sdclem1  37856  fdc  37858  istotbnd3  37884  sstotbnd2  37887  prdsbnd2  37908  heibor1lem  37922  heiborlem1  37924  heiborlem10  37933  heibor  37934  riscer  38101  divrngidl  38141  iss2  38449  eqvreldisj  38783  disjlem17  38970  prtlem17  39048  ax12eq  39113  ax12el  39114  ax12inda  39120  ax12v2-o  39121  osumcllem8N  40135  pexmidlem5N  40146  mapdrvallem2  41817  sn-sup2  42661  onexomgt  43398  onexoegt  43401  omabs2  43489  clcnvlem  43780  onfrALT  44706  chordthmALT  45089  relpmin  45109  relpfrlem  45110  modelaxreplem1  45135  wfac8prim  45159  snelmap  45243  ssnnf1octb  45354  choicefi  45360  mapss2  45365  difmap  45367  axccdom  45382  infxrlesupxr  45596  inficc  45696  fsumnncl  45734  stoweidlem43  46203  stoweidlem48  46208  stoweidlem57  46217  stoweidlem60  46220  qndenserrnopn  46458  issalnnd  46505  subsaliuncl  46518  sge0cl  46541  nnfoctbdj  46616  ismeannd  46627  caragenunicl  46684  isomennd  46691  ovn0lem  46725  ovnsubaddlem2  46731  hspdifhsp  46776  hspmbllem3  46788  smflimlem6  46936  smfpimbor1lem1  46958  smfpimcc  46968  smfsuplem2  46972  rlimdmafv  47339  dfatcolem  47417  rlimdmafv2  47420  grimuhgr  48049  grimcnv  48050  grimco  48051  uhgrimedgi  48052  isuspgrim0  48056  gricushgr  48079  gricsym  48083  uhgrimisgrgric  48093  clnbgrgrimlem  48095  clnbgrgrim  48096  grimedg  48097  grtriprop  48103  usgrgrtrirex  48112  isubgr3stgrlem3  48130  uspgrlim  48154  grlimprclnbgredg  48159  grlimgredgex  48162  grlimgrtri  48165  xpco2  49018  opnneilv  49070  thincciso  49614