Theorem exlimdv 1934

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2209. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1970, ax-7 2015. (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 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 1911

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

This theorem is referenced by:  exlimdvv  1935  exlimddv  1936  ax13lem1  2381  ax13  2382  nfeqf  2388  axc15  2433  sssn  4716  elpreqprb  4755  reusv2lem2  5268  ralxfr2d  5279  euotd  5372  wefrc  5518  wereu2  5521  releldmb  5787  relelrnb  5788  iss  5875  onfr  6208  dffv2  6747  dff3  6857  elunirn  7002  fsnex  7031  f1prex  7032  isomin  7084  isofrlem  7087  ovmpt4g  7292  soex  7631  f1oweALT  7677  op1steq  7737  fo2ndf  7822  mpoxopynvov0g  7890  reldmtpos  7910  rntpos  7915  wfrlem12  7976  wfrlem17  7981  erdisj  8351  map0g  8466  resixpfo  8518  domdifsn  8621  xpdom3  8636  domunsncan  8638  enfixsn  8647  sucdom2  8648  fodomr  8690  mapdom2  8710  mapdom3  8711  phplem4  8721  php3  8725  pssnn  8738  pssnnOLD  8774  ssfiOLD  8775  domfi  8776  findcard2OLD  8793  ac6sfi  8795  isfinite2  8809  xpfi  8822  domunfican  8824  fiint  8828  fodomfib  8831  mapfien2  8906  marypha1lem  8930  ordiso  9013  hartogslem1  9039  brwdom2  9070  wdomtr  9072  brwdom3  9079  unwdomg  9081  xpwdomg  9082  unxpwdom2  9085  inf3lem2  9125  epfrs  9206  tcmin  9216  cplem1  9351  pm54.43  9463  dfac8alem  9489  dfac8b  9491  dfac8clem  9492  ac10ct  9494  acni2  9506  acndom  9511  numwdom  9519  wdomfil  9521  wdomnumr  9524  iunfictbso  9574  dfac2b  9590  dfac9  9596  kmlem13  9622  djuinf  9648  fictb  9705  cfeq0  9716  cff1  9718  cfflb  9719  cofsmo  9729  cfsmolem  9730  coftr  9733  infpssr  9768  fin4en1  9769  fin23lem7  9776  isf34lem4  9837  axcc3  9898  domtriomlem  9902  axdc2lem  9908  axdc3lem2  9911  axdc3lem4  9913  axdc4lem  9915  ac6num  9939  ttukeylem6  9974  ttukeyg  9977  fodomb  9986  iundom2g  10000  alephreg  10042  fpwwe2lem10  10100  fpwwe2lem11  10101  canthp1  10114  pwfseq  10124  gruen  10272  grudomon  10277  gruina  10278  grur1  10280  ltexnq  10435  ltbtwnnq  10438  genpn0  10463  psslinpr  10491  prlem934  10493  ltaddpr  10494  ltexprlem2  10497  ltexprlem6  10501  ltexprlem7  10502  reclem2pr  10508  reclem4pr  10510  suplem1pr  10512  negn0  11107  sup2  11633  supaddc  11644  supmul1  11646  zsupss  12377  fiinfnf1o  13760  hasheqf1oi  13762  hashfun  13848  hashf1  13867  rtrclreclem3  14467  rlimdm  14956  climcau  15075  caucvgb  15084  summolem2  15121  zsum  15123  sumz  15127  fsumf1o  15128  fsumss  15130  fsumcl2lem  15136  fsumadd  15144  fsummulc2  15187  fsumconst  15193  fsumrelem  15210  ntrivcvg  15301  prodmolem2  15337  zprod  15339  prod1  15346  fprodf1o  15348  fprodss  15350  fprodcl2lem  15352  fprodmul  15362  fproddiv  15363  fprodconst  15380  fprodn0  15381  ruclem13  15643  4sqlem12  16347  vdwapun  16365  vdwlem9  16380  vdwlem10  16381  ramz  16416  ramub1  16419  firest  16764  mremre  16933  isacs2  16982  iscatd2  17010  cicsym  17133  sscfn1  17146  sscfn2  17147  initoeu2  17342  gsumval2a  17961  symggen  18665  cyggex2  19085  gsumval3  19095  gsumzres  19097  gsumzcl2  19098  gsumzf1o  19100  gsumzaddlem  19109  gsumconst  19122  gsumzmhm  19125  gsumzoppg  19132  gsum2d2  19162  pgpfac1lem5  19269  ablfaclem3  19277  lss0cl  19786  lspsnat  19985  cnsubrg  20226  gsumfsum  20233  obslbs  20495  lmiclbs  20602  lmisfree  20607  mdetdiaglem  21298  mdet0  21306  eltg3  21662  tgtop  21673  tgidm  21680  ppttop  21707  toponmre  21793  tgrest  21859  neitr  21880  tgcn  21952  cmpsublem  22099  cmpsub  22100  iunconnlem  22127  unconn  22129  1stcfb  22145  2ndcctbss  22155  2ndcdisj  22156  1stcelcls  22161  1stccnp  22162  locfincmp  22226  comppfsc  22232  1stckgen  22254  ptuni2  22276  ptbasfi  22281  ptpjopn  22312  ptclsg  22315  ptcnp  22322  prdstopn  22328  txindis  22334  txtube  22340  txcmplem1  22341  txcmplem2  22342  xkococnlem  22359  txconn  22389  trfbas2  22543  filtop  22555  filconn  22583  filssufilg  22611  fmfnfm  22658  ufldom  22662  hauspwpwf1  22687  alexsubALTlem3  22749  alexsubALT  22751  ptcmplem2  22753  tmdgsum2  22796  tgptsmscld  22851  ustfilxp  22913  xbln0  23116  opnreen  23532  metdsre  23554  cnheibor  23656  phtpc01  23697  cfilfcls  23974  cmetcaulem  23988  iscmet3  23993  ovolctb  24190  ovoliunlem3  24204  ovoliunnul  24207  ovolicc2lem5  24221  ovolicc2  24222  dyadmbl  24300  vitali  24313  itg11  24391  bddmulibl  24538  perfdvf  24602  dvcnp2  24619  dvlip  24692  dvne0  24710  fta1g  24867  fta1  25003  ulmcau  25089  pserulm  25116  wilthlem2  25753  dchrvmasumif  26186  rpvmasum2  26195  dchrisum0re  26196  dchrisum0lem3  26202  dchrisum0  26203  dchrmusum  26207  dchrvmasum  26208  axcontlem10  26866  usgr1v0e  27215  wlkiswwlks  27761  wlkiswwlkupgr  27763  wlklnwwlkn  27769  wlklnwwlknupgr  27771  umgrwwlks2on  27842  elwwlks2  27851  elwspths2spth  27852  clwlkclwwlklem3  27885  clwlkclwwlkfo  27893  frgr3vlem2  28158  spansncvi  29534  2ndresdju  30509  fnpreimac  30532  qsidomlem2  31150  reff  31310  locfinreflem  31311  cmpcref  31321  fmcncfil  31402  volmeas  31718  omssubadd  31786  bnj849  32425  acycgrislfgr  32630  derangenlem  32649  cvmsss2  32752  cvmopnlem  32756  cvmfolem  32757  cvmliftmolem2  32760  cvmliftlem15  32776  cvmlift2lem10  32790  cvmlift3lem8  32804  satfdmlem  32846  sat1el2xp  32857  fmlasuc  32864  fundmpss  33256  frpomin  33325  frmin  33334  frxp3  33352  frrlem10  33394  noinfno  33506  nocvxmin  33558  fnessref  34117  refssfne  34118  neibastop2lem  34120  neibastop2  34121  fnemeet2  34127  fnejoin2  34129  tailfb  34137  knoppcnlem9  34252  isinf2  35124  pibt2  35136  wl-ax13lem1  35213  wl-sbcom2d  35264  matunitlindflem2  35356  poimirlem25  35384  poimirlem27  35386  heicant  35394  itg2addnclem  35410  sdclem1  35483  fdc  35485  istotbnd3  35511  sstotbnd2  35514  prdsbnd2  35535  heibor1lem  35549  heiborlem1  35551  heiborlem10  35560  heibor  35561  riscer  35728  divrngidl  35768  iss2  36063  eqvreldisj  36311  prtlem17  36474  ax12eq  36539  ax12el  36540  ax12inda  36546  ax12v2-o  36547  osumcllem8N  37561  pexmidlem5N  37572  mapdrvallem2  39243  sn-sup2  39958  clcnvlem  40718  onfrALT  41650  chordthmALT  42034  snelmap  42113  ssnnf1octb  42214  choicefi  42221  mapss2  42226  difmap  42228  axccdom  42243  infxrlesupxr  42461  inficc  42559  fsumnncl  42601  stoweidlem43  43073  stoweidlem48  43078  stoweidlem57  43087  stoweidlem60  43090  qndenserrnopn  43328  issalnnd  43373  subsaliuncl  43386  sge0cl  43408  nnfoctbdj  43483  ismeannd  43494  caragenunicl  43551  isomennd  43558  ovn0lem  43592  ovnsubaddlem2  43598  hspdifhsp  43643  hspmbllem3  43655  smflimlem6  43797  smfpimbor1lem1  43818  smfpimcc  43827  smfsuplem2  43831  rlimdmafv  44123  dfatcolem  44201  rlimdmafv2  44204  isomushgr  44733  isomuspgr  44741  isomgrsym  44743  isomgrtr  44746  mgmpropd  44784  c0snmgmhm  44927  opnneilv  45606