Theorem exlimdv 1933

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exlimdvv  1934  exlimddv  1935  ax13lem1  2373  ax13  2374  nfeqf  2380  axc15  2421  sssn  4793  elpreqprb  4835  reusv2lem2  5357  ralxfr2d  5368  euotd  5476  wefrc  5635  wereu2  5638  releldmb  5913  relelrnb  5914  iss  6009  frpomin  6316  onfr  6374  dffv2  6959  dff3  7075  elunirn  7228  fsnex  7261  f1prex  7262  isomin  7315  isofrlem  7318  ovmpt4g  7539  soex  7900  f1oweALT  7954  op1steq  8015  fo2ndf  8103  frxp3  8133  mpoxopynvov0g  8196  reldmtpos  8216  rntpos  8221  frrlem10  8277  fprresex  8292  erdisj  8731  map0g  8860  resixpfo  8912  domdifsn  9028  xpdom3  9044  domunsncan  9046  enfixsn  9055  sucdom2OLD  9056  fodomr  9098  mapdom2  9118  mapdom3  9119  rexdif1en  9128  pssnn  9138  ssfiALT  9144  domfi  9159  sucdom2  9173  phplem2  9175  php3  9179  0sdom1dom  9192  sdom1  9196  1sdom2dom  9201  ac6sfi  9238  isfinite2  9252  xpfiOLD  9277  domunfican  9279  fiint  9284  fiintOLD  9285  fodomfir  9286  fodomfib  9287  fodomfibOLD  9289  mapfien2  9367  marypha1lem  9391  ordiso  9476  hartogslem1  9502  brwdom2  9533  wdomtr  9535  brwdom3  9542  unwdomg  9544  xpwdomg  9545  unxpwdom2  9548  inf3lem2  9589  ttrclss  9680  dmttrcl  9681  rnttrcl  9682  ttrclselem2  9686  epfrs  9691  tcmin  9701  frmin  9709  cplem1  9849  pm54.43  9961  dfac8alem  9989  dfac8b  9991  dfac8clem  9992  ac10ct  9994  acni2  10006  acndom  10011  numwdom  10019  wdomfil  10021  wdomnumr  10024  iunfictbso  10074  dfac2b  10091  dfac9  10097  kmlem13  10123  djuinf  10149  fictb  10204  cfeq0  10216  cff1  10218  cfflb  10219  cofsmo  10229  cfsmolem  10230  coftr  10233  infpssr  10268  fin4en1  10269  fin23lem7  10276  isf34lem4  10337  axcc3  10398  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  ac6num  10439  ttukeylem6  10474  ttukeyg  10477  fodomb  10486  iundom2g  10500  alephreg  10542  fpwwe2lem10  10600  fpwwe2lem11  10601  canthp1  10614  pwfseq  10624  gruen  10772  grudomon  10777  gruina  10778  grur1  10780  ltexnq  10935  ltbtwnnq  10938  genpn0  10963  psslinpr  10991  prlem934  10993  ltaddpr  10994  ltexprlem2  10997  ltexprlem6  11001  ltexprlem7  11002  reclem2pr  11008  reclem4pr  11010  suplem1pr  11012  negn0  11614  sup2  12146  supaddc  12157  supmul1  12159  zsupss  12903  fiinfnf1o  14322  hasheqf1oi  14323  hashfun  14409  hashf1  14429  hash3tpexb  14466  rtrclreclem3  15033  rlimdm  15524  climcau  15644  caucvgb  15653  summolem2  15689  zsum  15691  sumz  15695  fsumf1o  15696  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumconst  15763  fsumrelem  15780  ntrivcvg  15870  prodmolem2  15908  zprod  15910  prod1  15917  fprodf1o  15919  fprodss  15921  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodconst  15951  fprodn0  15952  ruclem13  16217  4sqlem12  16934  vdwapun  16952  vdwlem9  16967  vdwlem10  16968  ramz  17003  ramub1  17006  firest  17402  mremre  17572  isacs2  17621  iscatd2  17649  cicsym  17773  sscfn1  17786  sscfn2  17787  initoeu2  17985  mgmpropd  18585  gsumval2a  18619  symggen  19407  cyggex2  19834  gsumval3  19844  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  gsum2d2  19911  pgpfac1lem5  20018  ablfaclem3  20026  c0snmgmhm  20378  lss0cl  20860  lspsnat  21062  cnsubrg  21351  gsumfsum  21358  obslbs  21646  lmiclbs  21753  lmisfree  21758  mdetdiaglem  22492  mdet0  22500  eltg3  22856  tgtop  22867  tgidm  22874  ppttop  22901  toponmre  22987  tgrest  23053  neitr  23074  tgcn  23146  cmpsublem  23293  cmpsub  23294  iunconnlem  23321  unconn  23323  1stcfb  23339  2ndcctbss  23349  2ndcdisj  23350  1stcelcls  23355  1stccnp  23356  locfincmp  23420  comppfsc  23426  1stckgen  23448  ptuni2  23470  ptbasfi  23475  ptpjopn  23506  ptclsg  23509  ptcnp  23516  prdstopn  23522  txindis  23528  txtube  23534  txcmplem1  23535  txcmplem2  23536  xkococnlem  23553  txconn  23583  trfbas2  23737  filtop  23749  filconn  23777  filssufilg  23805  fmfnfm  23852  ufldom  23856  hauspwpwf1  23881  alexsubALTlem3  23943  alexsubALT  23945  ptcmplem2  23947  tmdgsum2  23990  tgptsmscld  24045  ustfilxp  24107  xbln0  24309  opnreen  24727  metdsre  24749  cnheibor  24861  phtpc01  24902  cfilfcls  25181  cmetcaulem  25195  iscmet3  25200  ovolctb  25398  ovoliunlem3  25412  ovoliunnul  25415  ovolicc2lem5  25429  ovolicc2  25430  dyadmbl  25508  vitali  25521  itg11  25599  bddmulibl  25747  perfdvf  25811  dvcnp2  25828  dvcnp2OLD  25829  dvlip  25905  dvne0  25923  fta1g  26082  fta1  26223  ulmcau  26311  pserulm  26338  wilthlem2  26986  dchrvmasumif  27421  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem3  27437  dchrisum0  27438  dchrmusum  27442  dchrvmasum  27443  noinfno  27637  nocvxmin  27697  sltlpss  27826  axcontlem10  28907  usgr1v0e  29260  wlkiswwlks  29813  wlkiswwlkupgr  29815  wlklnwwlkn  29821  wlklnwwlknupgr  29823  umgrwwlks2on  29894  elwwlks2  29903  elwspths2spth  29904  clwlkclwwlklem3  29937  clwlkclwwlkfo  29945  frgr3vlem2  30210  spansncvi  31588  2ndresdju  32580  fnpreimac  32602  gsumwrd2dccatlem  33013  qsidomlem2  33431  reff  33836  locfinreflem  33837  cmpcref  33847  fmcncfil  33928  volmeas  34228  omssubadd  34298  bnj849  34922  acycgrislfgr  35146  derangenlem  35165  cvmsss2  35268  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem2  35276  cvmliftlem15  35292  cvmlift2lem10  35306  cvmlift3lem8  35320  satfdmlem  35362  sat1el2xp  35373  fmlasuc  35380  fundmpss  35761  fnessref  36352  refssfne  36353  neibastop2lem  36355  neibastop2  36356  fnemeet2  36362  fnejoin2  36364  tailfb  36372  knoppcnlem9  36496  isinf2  37400  pibt2  37412  wl-ax13lem1  37489  wl-sbcom2d  37556  matunitlindflem2  37618  poimirlem25  37646  poimirlem27  37648  heicant  37656  itg2addnclem  37672  sdclem1  37744  fdc  37746  istotbnd3  37772  sstotbnd2  37775  prdsbnd2  37796  heibor1lem  37810  heiborlem1  37812  heiborlem10  37821  heibor  37822  riscer  37989  divrngidl  38029  iss2  38333  eqvreldisj  38612  disjlem17  38798  prtlem17  38876  ax12eq  38941  ax12el  38942  ax12inda  38948  ax12v2-o  38949  osumcllem8N  39964  pexmidlem5N  39975  mapdrvallem2  41646  sn-sup2  42486  onexomgt  43237  onexoegt  43240  omabs2  43328  clcnvlem  43619  onfrALT  44546  chordthmALT  44929  relpmin  44949  relpfrlem  44950  modelaxreplem1  44975  wfac8prim  44999  snelmap  45083  ssnnf1octb  45195  choicefi  45201  mapss2  45206  difmap  45208  axccdom  45223  infxrlesupxr  45439  inficc  45539  fsumnncl  45577  stoweidlem43  46048  stoweidlem48  46053  stoweidlem57  46062  stoweidlem60  46065  qndenserrnopn  46303  issalnnd  46350  subsaliuncl  46363  sge0cl  46386  nnfoctbdj  46461  ismeannd  46472  caragenunicl  46529  isomennd  46536  ovn0lem  46570  ovnsubaddlem2  46576  hspdifhsp  46621  hspmbllem3  46633  smflimlem6  46781  smfpimbor1lem1  46803  smfpimcc  46813  smfsuplem2  46817  rlimdmafv  47182  dfatcolem  47260  rlimdmafv2  47263  grimuhgr  47891  grimcnv  47892  grimco  47893  uhgrimedgi  47894  isuspgrim0  47898  gricushgr  47921  gricsym  47925  uhgrimisgrgric  47935  clnbgrgrimlem  47937  clnbgrgrim  47938  grimedg  47939  grtriprop  47944  usgrgrtrirex  47953  isubgr3stgrlem3  47971  uspgrlim  47995  grlimgrtri  47999  xpco2  48849  opnneilv  48901  thincciso  49446