Theorem exlimdv 1930

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

Syntax hints:   → wi 4  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  exlimdvv  1931  exlimddv  1932  ax13lem1  2376  ax13  2377  nfeqf  2383  axc15  2424  sssn  4830  elpreqprb  4872  reusv2lem2  5404  ralxfr2d  5415  euotd  5522  wefrc  5682  wereu2  5685  releldmb  5959  relelrnb  5960  iss  6054  frpomin  6362  onfr  6424  dffv2  7003  dff3  7119  elunirn  7270  fsnex  7302  f1prex  7303  isomin  7356  isofrlem  7359  ovmpt4g  7579  soex  7943  f1oweALT  7995  op1steq  8056  fo2ndf  8144  frxp3  8174  mpoxopynvov0g  8237  reldmtpos  8257  rntpos  8262  frrlem10  8318  fprresex  8333  wfrlem12OLD  8358  wfrlem17OLD  8363  erdisj  8797  map0g  8922  resixpfo  8974  domdifsn  9092  xpdom3  9108  domunsncan  9110  enfixsn  9119  sucdom2OLD  9120  fodomr  9166  mapdom2  9186  mapdom3  9187  rexdif1en  9196  pssnn  9206  ssfiALT  9212  domfi  9226  sucdom2  9240  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  0sdom1dom  9271  sdom1  9275  1sdom2dom  9280  ac6sfi  9317  isfinite2  9331  xpfiOLD  9356  domunfican  9358  fiint  9363  fiintOLD  9364  fodomfir  9365  fodomfib  9366  fodomfibOLD  9368  mapfien2  9446  marypha1lem  9470  ordiso  9553  hartogslem1  9579  brwdom2  9610  wdomtr  9612  brwdom3  9619  unwdomg  9621  xpwdomg  9622  unxpwdom2  9625  inf3lem2  9666  ttrclss  9757  dmttrcl  9758  rnttrcl  9759  ttrclselem2  9763  epfrs  9768  tcmin  9778  frmin  9786  cplem1  9926  pm54.43  10038  dfac8alem  10066  dfac8b  10068  dfac8clem  10069  ac10ct  10071  acni2  10083  acndom  10088  numwdom  10096  wdomfil  10098  wdomnumr  10101  iunfictbso  10151  dfac2b  10168  dfac9  10174  kmlem13  10200  djuinf  10226  fictb  10281  cfeq0  10293  cff1  10295  cfflb  10296  cofsmo  10306  cfsmolem  10307  coftr  10310  infpssr  10345  fin4en1  10346  fin23lem7  10353  isf34lem4  10414  axcc3  10475  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  ac6num  10516  ttukeylem6  10551  ttukeyg  10554  fodomb  10563  iundom2g  10577  alephreg  10619  fpwwe2lem10  10677  fpwwe2lem11  10678  canthp1  10691  pwfseq  10701  gruen  10849  grudomon  10854  gruina  10855  grur1  10857  ltexnq  11012  ltbtwnnq  11015  genpn0  11040  psslinpr  11068  prlem934  11070  ltaddpr  11071  ltexprlem2  11074  ltexprlem6  11078  ltexprlem7  11079  reclem2pr  11085  reclem4pr  11087  suplem1pr  11089  negn0  11689  sup2  12221  supaddc  12232  supmul1  12234  zsupss  12976  fiinfnf1o  14385  hasheqf1oi  14386  hashfun  14472  hashf1  14492  hash3tpexb  14529  rtrclreclem3  15095  rlimdm  15583  climcau  15703  caucvgb  15712  summolem2  15748  zsum  15750  sumz  15754  fsumf1o  15755  fsumss  15757  fsumcl2lem  15763  fsumadd  15772  fsummulc2  15816  fsumconst  15822  fsumrelem  15839  ntrivcvg  15929  prodmolem2  15967  zprod  15969  prod1  15976  fprodf1o  15978  fprodss  15980  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodconst  16010  fprodn0  16011  ruclem13  16274  4sqlem12  16989  vdwapun  17007  vdwlem9  17022  vdwlem10  17023  ramz  17058  ramub1  17061  firest  17478  mremre  17648  isacs2  17697  iscatd2  17725  cicsym  17851  sscfn1  17864  sscfn2  17865  initoeu2  18069  mgmpropd  18676  gsumval2a  18710  symggen  19502  cyggex2  19929  gsumval3  19939  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  gsumzoppg  19976  gsum2d2  20006  pgpfac1lem5  20113  ablfaclem3  20121  c0snmgmhm  20478  lss0cl  20962  lspsnat  21164  cnsubrg  21462  gsumfsum  21469  obslbs  21767  lmiclbs  21874  lmisfree  21879  mdetdiaglem  22619  mdet0  22627  eltg3  22984  tgtop  22995  tgidm  23002  ppttop  23029  toponmre  23116  tgrest  23182  neitr  23203  tgcn  23275  cmpsublem  23422  cmpsub  23423  iunconnlem  23450  unconn  23452  1stcfb  23468  2ndcctbss  23478  2ndcdisj  23479  1stcelcls  23484  1stccnp  23485  locfincmp  23549  comppfsc  23555  1stckgen  23577  ptuni2  23599  ptbasfi  23604  ptpjopn  23635  ptclsg  23638  ptcnp  23645  prdstopn  23651  txindis  23657  txtube  23663  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  txconn  23712  trfbas2  23866  filtop  23878  filconn  23906  filssufilg  23934  fmfnfm  23981  ufldom  23985  hauspwpwf1  24010  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem2  24076  tmdgsum2  24119  tgptsmscld  24174  ustfilxp  24236  xbln0  24439  opnreen  24866  metdsre  24888  cnheibor  25000  phtpc01  25041  cfilfcls  25321  cmetcaulem  25335  iscmet3  25340  ovolctb  25538  ovoliunlem3  25552  ovoliunnul  25555  ovolicc2lem5  25569  ovolicc2  25570  dyadmbl  25648  vitali  25661  itg11  25739  bddmulibl  25888  perfdvf  25952  dvcnp2  25969  dvcnp2OLD  25970  dvlip  26046  dvne0  26064  fta1g  26223  fta1  26364  ulmcau  26452  pserulm  26479  wilthlem2  27126  dchrvmasumif  27561  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem3  27577  dchrisum0  27578  dchrmusum  27582  dchrvmasum  27583  noinfno  27777  nocvxmin  27837  sltlpss  27959  axcontlem10  29002  usgr1v0e  29357  wlkiswwlks  29905  wlkiswwlkupgr  29907  wlklnwwlkn  29913  wlklnwwlknupgr  29915  umgrwwlks2on  29986  elwwlks2  29995  elwspths2spth  29996  clwlkclwwlklem3  30029  clwlkclwwlkfo  30037  frgr3vlem2  30302  spansncvi  31680  2ndresdju  32665  fnpreimac  32687  gsumwrd2dccatlem  33051  qsidomlem2  33460  reff  33799  locfinreflem  33800  cmpcref  33810  fmcncfil  33891  volmeas  34211  omssubadd  34281  bnj849  34917  acycgrislfgr  35136  derangenlem  35155  cvmsss2  35258  cvmopnlem  35262  cvmfolem  35263  cvmliftmolem2  35266  cvmliftlem15  35282  cvmlift2lem10  35296  cvmlift3lem8  35310  satfdmlem  35352  sat1el2xp  35363  fmlasuc  35370  fundmpss  35747  fnessref  36339  refssfne  36340  neibastop2lem  36342  neibastop2  36343  fnemeet2  36349  fnejoin2  36351  tailfb  36359  knoppcnlem9  36483  isinf2  37387  pibt2  37399  wl-ax13lem1  37476  wl-sbcom2d  37541  matunitlindflem2  37603  poimirlem25  37631  poimirlem27  37633  heicant  37641  itg2addnclem  37657  sdclem1  37729  fdc  37731  istotbnd3  37757  sstotbnd2  37760  prdsbnd2  37781  heibor1lem  37795  heiborlem1  37797  heiborlem10  37806  heibor  37807  riscer  37974  divrngidl  38014  iss2  38325  eqvreldisj  38595  disjlem17  38780  prtlem17  38857  ax12eq  38922  ax12el  38923  ax12inda  38929  ax12v2-o  38930  osumcllem8N  39945  pexmidlem5N  39956  mapdrvallem2  41627  sn-sup2  42477  onexomgt  43229  onexoegt  43232  omabs2  43321  clcnvlem  43612  onfrALT  44546  chordthmALT  44930  modelaxreplem1  44942  snelmap  45021  ssnnf1octb  45136  choicefi  45142  mapss2  45147  difmap  45149  axccdom  45164  infxrlesupxr  45385  inficc  45486  fsumnncl  45527  stoweidlem43  45998  stoweidlem48  46003  stoweidlem57  46012  stoweidlem60  46015  qndenserrnopn  46253  issalnnd  46300  subsaliuncl  46313  sge0cl  46336  nnfoctbdj  46411  ismeannd  46422  caragenunicl  46479  isomennd  46486  ovn0lem  46520  ovnsubaddlem2  46526  hspdifhsp  46571  hspmbllem3  46583  smflimlem6  46731  smfpimbor1lem1  46753  smfpimcc  46763  smfsuplem2  46767  rlimdmafv  47126  dfatcolem  47204  rlimdmafv2  47207  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  grimco  47817  gricushgr  47823  gricsym  47827  uhgrimisgrgric  47836  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  grtriprop  47845  usgrgrtrirex  47852  isubgr3stgrlem3  47870  uspgrlim  47894  grlimgrtri  47898  opnneilv  48704  thincciso  48848