Theorem exlimdv 1932

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 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 1916	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1911	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  exlimdvv  1933  exlimddv  1934  ax13lem1  2382  ax13  2383  nfeqf  2389  axc15  2430  sssn  4851  elpreqprb  4892  reusv2lem2  5417  ralxfr2d  5428  euotd  5532  wefrc  5694  wereu2  5697  releldmb  5971  relelrnb  5972  iss  6064  frpomin  6372  onfr  6434  dffv2  7017  dff3  7134  elunirn  7288  fsnex  7319  f1prex  7320  isomin  7373  isofrlem  7376  ovmpt4g  7597  soex  7961  f1oweALT  8013  op1steq  8074  fo2ndf  8162  frxp3  8192  mpoxopynvov0g  8255  reldmtpos  8275  rntpos  8280  frrlem10  8336  fprresex  8351  wfrlem12OLD  8376  wfrlem17OLD  8381  erdisj  8817  map0g  8942  resixpfo  8994  domdifsn  9120  xpdom3  9136  domunsncan  9138  enfixsn  9147  sucdom2OLD  9148  fodomr  9194  mapdom2  9214  mapdom3  9215  rexdif1en  9224  pssnn  9234  ssfiALT  9241  domfi  9255  sucdom2  9269  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  0sdom1dom  9301  sdom1  9305  1sdom2dom  9310  ac6sfi  9348  isfinite2  9362  xpfiOLD  9387  domunfican  9389  fiint  9394  fiintOLD  9395  fodomfir  9396  fodomfib  9397  fodomfibOLD  9399  mapfien2  9478  marypha1lem  9502  ordiso  9585  hartogslem1  9611  brwdom2  9642  wdomtr  9644  brwdom3  9651  unwdomg  9653  xpwdomg  9654  unxpwdom2  9657  inf3lem2  9698  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  epfrs  9800  tcmin  9810  frmin  9818  cplem1  9958  pm54.43  10070  dfac8alem  10098  dfac8b  10100  dfac8clem  10101  ac10ct  10103  acni2  10115  acndom  10120  numwdom  10128  wdomfil  10130  wdomnumr  10133  iunfictbso  10183  dfac2b  10200  dfac9  10206  kmlem13  10232  djuinf  10258  fictb  10313  cfeq0  10325  cff1  10327  cfflb  10328  cofsmo  10338  cfsmolem  10339  coftr  10342  infpssr  10377  fin4en1  10378  fin23lem7  10385  isf34lem4  10446  axcc3  10507  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  ac6num  10548  ttukeylem6  10583  ttukeyg  10586  fodomb  10595  iundom2g  10609  alephreg  10651  fpwwe2lem10  10709  fpwwe2lem11  10710  canthp1  10723  pwfseq  10733  gruen  10881  grudomon  10886  gruina  10887  grur1  10889  ltexnq  11044  ltbtwnnq  11047  genpn0  11072  psslinpr  11100  prlem934  11102  ltaddpr  11103  ltexprlem2  11106  ltexprlem6  11110  ltexprlem7  11111  reclem2pr  11117  reclem4pr  11119  suplem1pr  11121  negn0  11719  sup2  12251  supaddc  12262  supmul1  12264  zsupss  13002  fiinfnf1o  14399  hasheqf1oi  14400  hashfun  14486  hashf1  14506  hash3tpexb  14543  rtrclreclem3  15109  rlimdm  15597  climcau  15719  caucvgb  15728  summolem2  15764  zsum  15766  sumz  15770  fsumf1o  15771  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  fsummulc2  15832  fsumconst  15838  fsumrelem  15855  ntrivcvg  15945  prodmolem2  15983  zprod  15985  prod1  15992  fprodf1o  15994  fprodss  15996  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodconst  16026  fprodn0  16027  ruclem13  16290  4sqlem12  17003  vdwapun  17021  vdwlem9  17036  vdwlem10  17037  ramz  17072  ramub1  17075  firest  17492  mremre  17662  isacs2  17711  iscatd2  17739  cicsym  17865  sscfn1  17878  sscfn2  17879  initoeu2  18083  mgmpropd  18689  gsumval2a  18723  symggen  19512  cyggex2  19939  gsumval3  19949  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  gsum2d2  20016  pgpfac1lem5  20123  ablfaclem3  20131  c0snmgmhm  20488  lss0cl  20968  lspsnat  21170  cnsubrg  21468  gsumfsum  21475  obslbs  21773  lmiclbs  21880  lmisfree  21885  mdetdiaglem  22625  mdet0  22633  eltg3  22990  tgtop  23001  tgidm  23008  ppttop  23035  toponmre  23122  tgrest  23188  neitr  23209  tgcn  23281  cmpsublem  23428  cmpsub  23429  iunconnlem  23456  unconn  23458  1stcfb  23474  2ndcctbss  23484  2ndcdisj  23485  1stcelcls  23490  1stccnp  23491  locfincmp  23555  comppfsc  23561  1stckgen  23583  ptuni2  23605  ptbasfi  23610  ptpjopn  23641  ptclsg  23644  ptcnp  23651  prdstopn  23657  txindis  23663  txtube  23669  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  txconn  23718  trfbas2  23872  filtop  23884  filconn  23912  filssufilg  23940  fmfnfm  23987  ufldom  23991  hauspwpwf1  24016  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem2  24082  tmdgsum2  24125  tgptsmscld  24180  ustfilxp  24242  xbln0  24445  opnreen  24872  metdsre  24894  cnheibor  25006  phtpc01  25047  cfilfcls  25327  cmetcaulem  25341  iscmet3  25346  ovolctb  25544  ovoliunlem3  25558  ovoliunnul  25561  ovolicc2lem5  25575  ovolicc2  25576  dyadmbl  25654  vitali  25667  itg11  25745  bddmulibl  25894  perfdvf  25958  dvcnp2  25975  dvcnp2OLD  25976  dvlip  26052  dvne0  26070  fta1g  26229  fta1  26368  ulmcau  26456  pserulm  26483  wilthlem2  27130  dchrvmasumif  27565  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem3  27581  dchrisum0  27582  dchrmusum  27586  dchrvmasum  27587  noinfno  27781  nocvxmin  27841  sltlpss  27963  axcontlem10  29006  usgr1v0e  29361  wlkiswwlks  29909  wlkiswwlkupgr  29911  wlklnwwlkn  29917  wlklnwwlknupgr  29919  umgrwwlks2on  29990  elwwlks2  29999  elwspths2spth  30000  clwlkclwwlklem3  30033  clwlkclwwlkfo  30041  frgr3vlem2  30306  spansncvi  31684  2ndresdju  32667  fnpreimac  32689  qsidomlem2  33446  reff  33785  locfinreflem  33786  cmpcref  33796  fmcncfil  33877  volmeas  34195  omssubadd  34265  bnj849  34901  acycgrislfgr  35120  derangenlem  35139  cvmsss2  35242  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem10  35280  cvmlift3lem8  35294  satfdmlem  35336  sat1el2xp  35347  fmlasuc  35354  fundmpss  35730  fnessref  36323  refssfne  36324  neibastop2lem  36326  neibastop2  36327  fnemeet2  36333  fnejoin2  36335  tailfb  36343  knoppcnlem9  36467  isinf2  37371  pibt2  37383  wl-ax13lem1  37460  wl-sbcom2d  37515  matunitlindflem2  37577  poimirlem25  37605  poimirlem27  37607  heicant  37615  itg2addnclem  37631  sdclem1  37703  fdc  37705  istotbnd3  37731  sstotbnd2  37734  prdsbnd2  37755  heibor1lem  37769  heiborlem1  37771  heiborlem10  37780  heibor  37781  riscer  37948  divrngidl  37988  iss2  38300  eqvreldisj  38570  disjlem17  38755  prtlem17  38832  ax12eq  38897  ax12el  38898  ax12inda  38904  ax12v2-o  38905  osumcllem8N  39920  pexmidlem5N  39931  mapdrvallem2  41602  sn-sup2  42447  onexomgt  43202  onexoegt  43205  omabs2  43294  clcnvlem  43585  onfrALT  44520  chordthmALT  44904  snelmap  44984  ssnnf1octb  45101  choicefi  45107  mapss2  45112  difmap  45114  axccdom  45129  infxrlesupxr  45351  inficc  45452  fsumnncl  45493  stoweidlem43  45964  stoweidlem48  45969  stoweidlem57  45978  stoweidlem60  45981  qndenserrnopn  46219  issalnnd  46266  subsaliuncl  46279  sge0cl  46302  nnfoctbdj  46377  ismeannd  46388  caragenunicl  46445  isomennd  46452  ovn0lem  46486  ovnsubaddlem2  46492  hspdifhsp  46537  hspmbllem3  46549  smflimlem6  46697  smfpimbor1lem1  46719  smfpimcc  46729  smfsuplem2  46733  rlimdmafv  47092  dfatcolem  47170  rlimdmafv2  47173  isuspgrim0  47756  grimuhgr  47762  grimcnv  47763  grimco  47764  gricushgr  47770  gricsym  47774  uhgrimisgrgric  47783  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  grtriprop  47792  usgrgrtrirex  47799  uspgrlim  47816  grlimgrtri  47820  opnneilv  48588  thincciso  48716