Theorem exlimdv 1933

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2211. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1967, ax-7 2007. (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  2379  ax13  2380  nfeqf  2386  axc15  2427  sssn  4826  elpreqprb  4868  reusv2lem2  5399  ralxfr2d  5410  euotd  5518  wefrc  5679  wereu2  5682  releldmb  5957  relelrnb  5958  iss  6053  frpomin  6361  onfr  6423  dffv2  7004  dff3  7120  elunirn  7271  fsnex  7303  f1prex  7304  isomin  7357  isofrlem  7360  ovmpt4g  7580  soex  7943  f1oweALT  7997  op1steq  8058  fo2ndf  8146  frxp3  8176  mpoxopynvov0g  8239  reldmtpos  8259  rntpos  8264  frrlem10  8320  fprresex  8335  wfrlem12OLD  8360  wfrlem17OLD  8365  erdisj  8799  map0g  8924  resixpfo  8976  domdifsn  9094  xpdom3  9110  domunsncan  9112  enfixsn  9121  sucdom2OLD  9122  fodomr  9168  mapdom2  9188  mapdom3  9189  rexdif1en  9198  pssnn  9208  ssfiALT  9214  domfi  9229  sucdom2  9243  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  0sdom1dom  9274  sdom1  9278  1sdom2dom  9283  ac6sfi  9320  isfinite2  9334  xpfiOLD  9359  domunfican  9361  fiint  9366  fiintOLD  9367  fodomfir  9368  fodomfib  9369  fodomfibOLD  9371  mapfien2  9449  marypha1lem  9473  ordiso  9556  hartogslem1  9582  brwdom2  9613  wdomtr  9615  brwdom3  9622  unwdomg  9624  xpwdomg  9625  unxpwdom2  9628  inf3lem2  9669  ttrclss  9760  dmttrcl  9761  rnttrcl  9762  ttrclselem2  9766  epfrs  9771  tcmin  9781  frmin  9789  cplem1  9929  pm54.43  10041  dfac8alem  10069  dfac8b  10071  dfac8clem  10072  ac10ct  10074  acni2  10086  acndom  10091  numwdom  10099  wdomfil  10101  wdomnumr  10104  iunfictbso  10154  dfac2b  10171  dfac9  10177  kmlem13  10203  djuinf  10229  fictb  10284  cfeq0  10296  cff1  10298  cfflb  10299  cofsmo  10309  cfsmolem  10310  coftr  10313  infpssr  10348  fin4en1  10349  fin23lem7  10356  isf34lem4  10417  axcc3  10478  domtriomlem  10482  axdc2lem  10488  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  ac6num  10519  ttukeylem6  10554  ttukeyg  10557  fodomb  10566  iundom2g  10580  alephreg  10622  fpwwe2lem10  10680  fpwwe2lem11  10681  canthp1  10694  pwfseq  10704  gruen  10852  grudomon  10857  gruina  10858  grur1  10860  ltexnq  11015  ltbtwnnq  11018  genpn0  11043  psslinpr  11071  prlem934  11073  ltaddpr  11074  ltexprlem2  11077  ltexprlem6  11081  ltexprlem7  11082  reclem2pr  11088  reclem4pr  11090  suplem1pr  11092  negn0  11692  sup2  12224  supaddc  12235  supmul1  12237  zsupss  12979  fiinfnf1o  14389  hasheqf1oi  14390  hashfun  14476  hashf1  14496  hash3tpexb  14533  rtrclreclem3  15099  rlimdm  15587  climcau  15707  caucvgb  15716  summolem2  15752  zsum  15754  sumz  15758  fsumf1o  15759  fsumss  15761  fsumcl2lem  15767  fsumadd  15776  fsummulc2  15820  fsumconst  15826  fsumrelem  15843  ntrivcvg  15933  prodmolem2  15971  zprod  15973  prod1  15980  fprodf1o  15982  fprodss  15984  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodconst  16014  fprodn0  16015  ruclem13  16278  4sqlem12  16994  vdwapun  17012  vdwlem9  17027  vdwlem10  17028  ramz  17063  ramub1  17066  firest  17477  mremre  17647  isacs2  17696  iscatd2  17724  cicsym  17848  sscfn1  17861  sscfn2  17862  initoeu2  18061  mgmpropd  18664  gsumval2a  18698  symggen  19488  cyggex2  19915  gsumval3  19925  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  gsum2d2  19992  pgpfac1lem5  20099  ablfaclem3  20107  c0snmgmhm  20462  lss0cl  20945  lspsnat  21147  cnsubrg  21445  gsumfsum  21452  obslbs  21750  lmiclbs  21857  lmisfree  21862  mdetdiaglem  22604  mdet0  22612  eltg3  22969  tgtop  22980  tgidm  22987  ppttop  23014  toponmre  23101  tgrest  23167  neitr  23188  tgcn  23260  cmpsublem  23407  cmpsub  23408  iunconnlem  23435  unconn  23437  1stcfb  23453  2ndcctbss  23463  2ndcdisj  23464  1stcelcls  23469  1stccnp  23470  locfincmp  23534  comppfsc  23540  1stckgen  23562  ptuni2  23584  ptbasfi  23589  ptpjopn  23620  ptclsg  23623  ptcnp  23630  prdstopn  23636  txindis  23642  txtube  23648  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  txconn  23697  trfbas2  23851  filtop  23863  filconn  23891  filssufilg  23919  fmfnfm  23966  ufldom  23970  hauspwpwf1  23995  alexsubALTlem3  24057  alexsubALT  24059  ptcmplem2  24061  tmdgsum2  24104  tgptsmscld  24159  ustfilxp  24221  xbln0  24424  opnreen  24853  metdsre  24875  cnheibor  24987  phtpc01  25028  cfilfcls  25308  cmetcaulem  25322  iscmet3  25327  ovolctb  25525  ovoliunlem3  25539  ovoliunnul  25542  ovolicc2lem5  25556  ovolicc2  25557  dyadmbl  25635  vitali  25648  itg11  25726  bddmulibl  25874  perfdvf  25938  dvcnp2  25955  dvcnp2OLD  25956  dvlip  26032  dvne0  26050  fta1g  26209  fta1  26350  ulmcau  26438  pserulm  26465  wilthlem2  27112  dchrvmasumif  27547  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  dchrmusum  27568  dchrvmasum  27569  noinfno  27763  nocvxmin  27823  sltlpss  27945  axcontlem10  28988  usgr1v0e  29343  wlkiswwlks  29896  wlkiswwlkupgr  29898  wlklnwwlkn  29904  wlklnwwlknupgr  29906  umgrwwlks2on  29977  elwwlks2  29986  elwspths2spth  29987  clwlkclwwlklem3  30020  clwlkclwwlkfo  30028  frgr3vlem2  30293  spansncvi  31671  2ndresdju  32659  fnpreimac  32681  gsumwrd2dccatlem  33069  qsidomlem2  33481  reff  33838  locfinreflem  33839  cmpcref  33849  fmcncfil  33930  volmeas  34232  omssubadd  34302  bnj849  34939  acycgrislfgr  35157  derangenlem  35176  cvmsss2  35279  cvmopnlem  35283  cvmfolem  35284  cvmliftmolem2  35287  cvmliftlem15  35303  cvmlift2lem10  35317  cvmlift3lem8  35331  satfdmlem  35373  sat1el2xp  35384  fmlasuc  35391  fundmpss  35767  fnessref  36358  refssfne  36359  neibastop2lem  36361  neibastop2  36362  fnemeet2  36368  fnejoin2  36370  tailfb  36378  knoppcnlem9  36502  isinf2  37406  pibt2  37418  wl-ax13lem1  37495  wl-sbcom2d  37562  matunitlindflem2  37624  poimirlem25  37652  poimirlem27  37654  heicant  37662  itg2addnclem  37678  sdclem1  37750  fdc  37752  istotbnd3  37778  sstotbnd2  37781  prdsbnd2  37802  heibor1lem  37816  heiborlem1  37818  heiborlem10  37827  heibor  37828  riscer  37995  divrngidl  38035  iss2  38345  eqvreldisj  38615  disjlem17  38800  prtlem17  38877  ax12eq  38942  ax12el  38943  ax12inda  38949  ax12v2-o  38950  osumcllem8N  39965  pexmidlem5N  39976  mapdrvallem2  41647  sn-sup2  42501  onexomgt  43253  onexoegt  43256  omabs2  43345  clcnvlem  43636  onfrALT  44569  chordthmALT  44953  relpmin  44973  relpfrlem  44974  modelaxreplem1  44995  wfac8prim  45019  snelmap  45087  ssnnf1octb  45199  choicefi  45205  mapss2  45210  difmap  45212  axccdom  45227  infxrlesupxr  45447  inficc  45547  fsumnncl  45587  stoweidlem43  46058  stoweidlem48  46063  stoweidlem57  46072  stoweidlem60  46075  qndenserrnopn  46313  issalnnd  46360  subsaliuncl  46373  sge0cl  46396  nnfoctbdj  46471  ismeannd  46482  caragenunicl  46539  isomennd  46546  ovn0lem  46580  ovnsubaddlem2  46586  hspdifhsp  46631  hspmbllem3  46643  smflimlem6  46791  smfpimbor1lem1  46813  smfpimcc  46823  smfsuplem2  46827  rlimdmafv  47189  dfatcolem  47267  rlimdmafv2  47270  isuspgrim0  47872  grimuhgr  47878  grimcnv  47879  grimco  47880  gricushgr  47886  gricsym  47890  uhgrimisgrgric  47899  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  grtriprop  47908  usgrgrtrirex  47917  isubgr3stgrlem3  47935  uspgrlim  47959  grlimgrtri  47963  opnneilv  48806  thincciso  49102