Theorem exlimdv 1936

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  exlimdvv  1937  exlimddv  1938  ax13lem1  2372  ax13  2373  nfeqf  2379  axc15  2420  sssn  4822  elpreqprb  4861  reusv2lem2  5390  ralxfr2d  5401  euotd  5506  wefrc  5663  wereu2  5666  releldmb  5937  relelrnb  5938  iss  6025  frpomin  6330  onfr  6392  dffv2  6972  dff3  7086  elunirn  7234  fsnex  7265  f1prex  7266  isomin  7318  isofrlem  7321  ovmpt4g  7538  soex  7894  f1oweALT  7941  op1steq  8001  fo2ndf  8089  frxp3  8119  mpoxopynvov0g  8181  reldmtpos  8201  rntpos  8206  frrlem10  8262  fprresex  8277  wfrlem12OLD  8302  wfrlem17OLD  8307  erdisj  8738  map0g  8861  resixpfo  8913  domdifsn  9037  xpdom3  9053  domunsncan  9055  enfixsn  9064  sucdom2OLD  9065  fodomr  9111  mapdom2  9131  mapdom3  9132  rexdif1en  9141  pssnn  9151  ssfiALT  9157  domfi  9175  sucdom2  9189  phplem2  9191  php3  9195  phplem4OLD  9203  php3OLD  9207  0sdom1dom  9221  sdom1  9225  1sdom2dom  9230  pssnnOLD  9248  findcard2OLD  9267  ac6sfi  9270  isfinite2  9284  xpfiOLD  9301  domunfican  9303  fiint  9307  fodomfib  9309  mapfien2  9386  marypha1lem  9410  ordiso  9493  hartogslem1  9519  brwdom2  9550  wdomtr  9552  brwdom3  9559  unwdomg  9561  xpwdomg  9562  unxpwdom2  9565  inf3lem2  9606  ttrclss  9697  dmttrcl  9698  rnttrcl  9699  ttrclselem2  9703  epfrs  9708  tcmin  9718  frmin  9726  cplem1  9866  pm54.43  9978  dfac8alem  10006  dfac8b  10008  dfac8clem  10009  ac10ct  10011  acni2  10023  acndom  10028  numwdom  10036  wdomfil  10038  wdomnumr  10041  iunfictbso  10091  dfac2b  10107  dfac9  10113  kmlem13  10139  djuinf  10165  fictb  10222  cfeq0  10233  cff1  10235  cfflb  10236  cofsmo  10246  cfsmolem  10247  coftr  10250  infpssr  10285  fin4en1  10286  fin23lem7  10293  isf34lem4  10354  axcc3  10415  domtriomlem  10419  axdc2lem  10425  axdc3lem2  10428  axdc3lem4  10430  axdc4lem  10432  ac6num  10456  ttukeylem6  10491  ttukeyg  10494  fodomb  10503  iundom2g  10517  alephreg  10559  fpwwe2lem10  10617  fpwwe2lem11  10618  canthp1  10631  pwfseq  10641  gruen  10789  grudomon  10794  gruina  10795  grur1  10797  ltexnq  10952  ltbtwnnq  10955  genpn0  10980  psslinpr  11008  prlem934  11010  ltaddpr  11011  ltexprlem2  11014  ltexprlem6  11018  ltexprlem7  11019  reclem2pr  11025  reclem4pr  11027  suplem1pr  11029  negn0  11625  sup2  12152  supaddc  12163  supmul1  12165  zsupss  12903  fiinfnf1o  14292  hasheqf1oi  14293  hashfun  14379  hashf1  14400  rtrclreclem3  14989  rlimdm  15477  climcau  15599  caucvgb  15608  summolem2  15644  zsum  15646  sumz  15650  fsumf1o  15651  fsumss  15653  fsumcl2lem  15659  fsumadd  15668  fsummulc2  15712  fsumconst  15718  fsumrelem  15735  ntrivcvg  15825  prodmolem2  15861  zprod  15863  prod1  15870  fprodf1o  15872  fprodss  15874  fprodcl2lem  15876  fprodmul  15886  fproddiv  15887  fprodconst  15904  fprodn0  15905  ruclem13  16167  4sqlem12  16871  vdwapun  16889  vdwlem9  16904  vdwlem10  16905  ramz  16940  ramub1  16943  firest  17360  mremre  17530  isacs2  17579  iscatd2  17607  cicsym  17733  sscfn1  17746  sscfn2  17747  initoeu2  17948  gsumval2a  18586  symggen  19302  cyggex2  19724  gsumval3  19734  gsumzres  19736  gsumzcl2  19737  gsumzf1o  19739  gsumzaddlem  19748  gsumconst  19761  gsumzmhm  19764  gsumzoppg  19771  gsum2d2  19801  pgpfac1lem5  19908  ablfaclem3  19916  lss0cl  20506  lspsnat  20707  cnsubrg  20939  gsumfsum  20946  obslbs  21218  lmiclbs  21325  lmisfree  21330  mdetdiaglem  22029  mdet0  22037  eltg3  22394  tgtop  22405  tgidm  22412  ppttop  22439  toponmre  22526  tgrest  22592  neitr  22613  tgcn  22685  cmpsublem  22832  cmpsub  22833  iunconnlem  22860  unconn  22862  1stcfb  22878  2ndcctbss  22888  2ndcdisj  22889  1stcelcls  22894  1stccnp  22895  locfincmp  22959  comppfsc  22965  1stckgen  22987  ptuni2  23009  ptbasfi  23014  ptpjopn  23045  ptclsg  23048  ptcnp  23055  prdstopn  23061  txindis  23067  txtube  23073  txcmplem1  23074  txcmplem2  23075  xkococnlem  23092  txconn  23122  trfbas2  23276  filtop  23288  filconn  23316  filssufilg  23344  fmfnfm  23391  ufldom  23395  hauspwpwf1  23420  alexsubALTlem3  23482  alexsubALT  23484  ptcmplem2  23486  tmdgsum2  23529  tgptsmscld  23584  ustfilxp  23646  xbln0  23849  opnreen  24276  metdsre  24298  cnheibor  24400  phtpc01  24441  cfilfcls  24720  cmetcaulem  24734  iscmet3  24739  ovolctb  24936  ovoliunlem3  24950  ovoliunnul  24953  ovolicc2lem5  24967  ovolicc2  24968  dyadmbl  25046  vitali  25059  itg11  25137  bddmulibl  25285  perfdvf  25349  dvcnp2  25366  dvlip  25439  dvne0  25457  fta1g  25614  fta1  25750  ulmcau  25836  pserulm  25863  wilthlem2  26500  dchrvmasumif  26933  rpvmasum2  26942  dchrisum0re  26943  dchrisum0lem3  26949  dchrisum0  26950  dchrmusum  26954  dchrvmasum  26955  noinfno  27148  nocvxmin  27206  sltlpss  27324  axcontlem10  28096  usgr1v0e  28448  wlkiswwlks  28995  wlkiswwlkupgr  28997  wlklnwwlkn  29003  wlklnwwlknupgr  29005  umgrwwlks2on  29076  elwwlks2  29085  elwspths2spth  29086  clwlkclwwlklem3  29119  clwlkclwwlkfo  29127  frgr3vlem2  29392  spansncvi  30768  2ndresdju  31743  fnpreimac  31765  qsidomlem2  32421  reff  32648  locfinreflem  32649  cmpcref  32659  fmcncfil  32740  volmeas  33058  omssubadd  33128  bnj849  33765  acycgrislfgr  33972  derangenlem  33991  cvmsss2  34094  cvmopnlem  34098  cvmfolem  34099  cvmliftmolem2  34102  cvmliftlem15  34118  cvmlift2lem10  34132  cvmlift3lem8  34146  satfdmlem  34188  sat1el2xp  34199  fmlasuc  34206  fundmpss  34566  fnessref  35044  refssfne  35045  neibastop2lem  35047  neibastop2  35048  fnemeet2  35054  fnejoin2  35056  tailfb  35064  knoppcnlem9  35179  isinf2  36088  pibt2  36100  wl-ax13lem1  36177  wl-sbcom2d  36228  matunitlindflem2  36287  poimirlem25  36315  poimirlem27  36317  heicant  36325  itg2addnclem  36341  sdclem1  36414  fdc  36416  istotbnd3  36442  sstotbnd2  36445  prdsbnd2  36466  heibor1lem  36480  heiborlem1  36482  heiborlem10  36491  heibor  36492  riscer  36659  divrngidl  36699  iss2  37016  eqvreldisj  37287  disjlem17  37472  prtlem17  37549  ax12eq  37614  ax12el  37615  ax12inda  37621  ax12v2-o  37622  osumcllem8N  38637  pexmidlem5N  38648  mapdrvallem2  40319  sn-sup2  41122  onexomgt  41759  onexoegt  41762  omabs2  41851  clcnvlem  42143  onfrALT  43079  chordthmALT  43463  snelmap  43540  ssnnf1octb  43662  choicefi  43668  mapss2  43673  difmap  43675  axccdom  43690  infxrlesupxr  43917  inficc  44018  fsumnncl  44059  stoweidlem43  44530  stoweidlem48  44535  stoweidlem57  44544  stoweidlem60  44547  qndenserrnopn  44785  issalnnd  44832  subsaliuncl  44845  sge0cl  44868  nnfoctbdj  44943  ismeannd  44954  caragenunicl  45011  isomennd  45018  ovn0lem  45052  ovnsubaddlem2  45058  hspdifhsp  45103  hspmbllem3  45115  smflimlem6  45263  smfpimbor1lem1  45285  smfpimcc  45295  smfsuplem2  45299  rlimdmafv  45655  dfatcolem  45733  rlimdmafv2  45736  isomushgr  46264  isomuspgr  46272  isomgrsym  46274  isomgrtr  46277  mgmpropd  46315  c0snmgmhm  46458  opnneilv  47187  thincciso  47315