Theorem exlimdv 1966

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exlimdvv  1967  exlimddv  1968  ax13lem1  2408  ax13  2409  nfeqf  2415  axc15  2456  sssn  4794  elpreqprb  4835  reusv2lem2  5372  ralxfr2d  5383  euotd  5498  wefrc  5657  wereu2  5660  releldmb  5938  relelrnb  5939  iss  6039  frpomin  6345  onfr  6404  dffv2  6980  dff3  7099  elunirn  7251  fsnex  7287  f1prex  7288  isomin  7341  isofrlem  7344  ovmpt4g  7563  soex  7920  f1oweALT  7971  op1steq  8032  fo2ndf  8118  frxp3  8149  mpoxopynvov0g  8212  reldmtpos  8232  rntpos  8237  frrlem10  8294  fprresex  8309  erdisj  8754  map0g  8884  resixpfo  8936  domdifsn  9051  xpdom3  9066  domunsncan  9068  enfixsn  9077  fodomr  9119  mapdom2  9139  mapdom3  9140  rexdif1en  9148  pssnn  9156  ssfiALT  9161  domfi  9176  sucdom2  9190  phplem2  9192  php3  9196  0sdom1dom  9209  sdom1  9213  1sdom2dom  9217  ac6sfi  9247  isfinite2  9261  domunfican  9284  fiint  9289  fodomfir  9290  fodomfib  9291  mapfien2  9372  marypha1lem  9396  ordiso  9481  hartogslem1  9507  brwdom2  9538  wdomtr  9540  brwdom3  9547  unwdomg  9549  xpwdomg  9550  unxpwdom2  9553  inf3lem2  9601  ttrclss  9692  dmttrcl  9693  rnttrcl  9694  ttrclselem2  9698  epfrs  9703  tcmin  9711  frmin  9724  cplem1  9882  cplem1OLD  9883  karden  9891  pm54.43  9999  dfac8alem  10025  dfac8b  10027  dfac8clem  10028  ac10ct  10030  acni2  10042  acndom  10047  numwdom  10055  wdomfil  10057  wdomnumr  10060  iunfictbso  10110  dfac2b  10126  dfac9  10132  kmlem13  10158  djuinf  10184  fictb  10239  cfeq0  10251  cff1  10253  cfflb  10254  cofsmo  10264  cfsmolem  10265  coftr  10268  infpssr  10303  fin4en1  10304  fin23lem7  10311  isf34lem4  10372  axcc3  10433  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  ac6num  10474  ttukeylem6  10509  ttukeyg  10512  fodomb  10521  iundom2g  10535  alephreg  10578  fpwwe2lem10  10636  fpwwe2lem11  10637  canthp1  10650  pwfseq  10660  gruen  10808  grudomon  10813  gruina  10814  grur1  10816  ltexnq  10971  ltbtwnnq  10974  genpn0  10999  psslinpr  11027  prlem934  11029  ltaddpr  11030  ltexprlem2  11033  ltexprlem6  11037  ltexprlem7  11038  reclem2pr  11044  reclem4pr  11046  suplem1pr  11048  negn0  11654  sup2  12182  supaddc  12193  supmul1  12195  zsupss  12973  fiinfnf1o  14400  hasheqf1oi  14401  hashfun  14488  hashf1  14508  hash3tpexb  14545  rtrclreclem3  15117  rlimdm  15622  climcau  15742  caucvgb  15751  summolem2  15786  zsum  15788  sumz  15792  fsumf1o  15793  fsumss  15795  fsumcl2lem  15801  fsumadd  15810  fsummulc2  15854  fsumconst  15860  fsumrelem  15878  ntrivcvg  15970  prodmolem2  16008  zprod  16010  prod1  16017  fprodf1o  16019  fprodss  16021  fprodcl2lem  16023  fprodmul  16033  fproddiv  16034  fprodconst  16051  fprodn0  16052  ruclem13  16316  4sqlem12  17034  vdwapun  17052  vdwlem9  17067  vdwlem10  17068  ramz  17103  ramub1  17106  firest  17503  mremre  17674  isacs2  17727  iscatd2  17755  cicsym  17879  sscfn1  17892  sscfn2  17893  initoeu2  18091  mgmpropd  18727  gsumval2a  18765  symggen  19564  cyggex2  19991  gsumval3  20001  gsumzres  20003  gsumzcl2  20004  gsumzf1o  20006  gsumzaddlem  20015  gsumconst  20028  gsumzmhm  20031  gsumzoppg  20038  gsum2d2  20068  pgpfac1lem5  20175  ablfaclem3  20183  c0snmgmhm  20570  lss0cl  21098  lspsnat  21299  qsidomlem2  21511  cnsubrg  21607  gsumfsum  21614  obslbs  21910  lmiclbs  22017  lmisfree  22022  mdetdiaglem  22785  mdet0  22793  eltg3  23149  tgtop  23160  tgidm  23167  ppttop  23194  toponmre  23280  tgrest  23346  neitr  23367  tgcn  23439  cmpsublem  23586  cmpsub  23587  iunconnlem  23614  unconn  23616  1stcfb  23632  2ndcctbss  23643  2ndcdisj  23644  1stcelcls  23649  1stccnp  23650  locfincmp  23714  comppfsc  23720  1stckgen  23742  ptuni2  23764  ptbasfi  23769  ptpjopn  23800  ptclsg  23803  ptcnp  23810  prdstopn  23816  txindis  23822  txtube  23828  txcmplem1  23829  txcmplem2  23830  xkococnlem  23847  txconn  23877  trfbas2  24031  filtop  24043  filconn  24071  filssufilg  24099  fmfnfm  24146  ufldom  24150  hauspwpwf1  24175  alexsubALTlem3  24237  alexsubALT  24239  ptcmplem2  24241  tmdgsum2  24284  tgptsmscld  24339  ustfilxp  24401  xbln0  24602  opnreen  25020  metdsre  25042  cnheibor  25145  phtpc01  25186  cfilfcls  25464  cmetcaulem  25478  iscmet3  25483  ovolctb  25680  ovoliunlem3  25694  ovoliunnul  25697  ovolicc2lem5  25711  ovolicc2  25712  dyadmbl  25790  vitali  25803  itg11  25881  bddmulibl  26029  perfdvf  26093  dvcnp2  26110  dvlip  26183  dvne0  26201  fta1g  26358  fta1  26500  ulmcau  26589  pserulm  26616  wilthlem2  27264  dchrvmasumif  27698  rpvmasum2  27707  dchrisum0re  27708  dchrisum0lem3  27714  dchrisum0  27715  dchrmusum  27719  dchrvmasum  27720  noinfno  27913  nobdaymin  27977  ltslpss  28132  axcontlem10  29354  usgr1v0e  29710  wlkiswwlks  30268  wlkiswwlkupgr  30270  wlklnwwlkn  30276  wlklnwwlknupgr  30278  usgrwwlks2on  30350  umgrwwlks2on  30351  elwwlks2  30361  elwspths2spth  30362  clwlkclwwlklem3  30395  clwlkclwwlkfo  30403  frgr3vlem2  30672  spansncvi  32051  2ndresdju  33041  fnpreimac  33062  gsumwrd2dccatlem  33437  reff  34269  locfinreflem  34270  cmpcref  34280  fmcncfil  34361  volmeas  34662  omssubadd  34731  bnj849  35354  r1filimi  35531  kardfi  35616  onvfowev  35633  acycgrislfgr  35657  derangenlem  35676  cvmsss2  35779  cvmopnlem  35783  cvmfolem  35784  cvmliftmolem2  35787  cvmliftlem15  35803  cvmlift2lem10  35817  cvmlift3lem8  35831  satfdmlem  35873  sat1el2xp  35884  fmlasuc  35891  fundmpss  36272  fnessref  36901  refssfne  36902  neibastop2lem  36904  neibastop2  36905  fnemeet2  36911  fnejoin2  36913  tailfb  36921  axuntco  37023  dfttc4lem2  37073  knoppcnlem9  37123  isinf2  38084  pibt2  38096  wl-ax13lem1  38173  wl-sbcom2d  38249  matunitlindflem2  38301  poimirlem25  38329  poimirlem27  38331  heicant  38339  itg2addnclem  38355  sdclem1  38427  fdc  38429  istotbnd3  38455  sstotbnd2  38458  prdsbnd2  38479  heibor1lem  38493  heiborlem1  38495  heiborlem10  38504  heibor  38505  riscer  38672  divrngidl  38712  iss2  39026  eqvreldisj  39380  disjlem17  39584  prtlem17  39683  ax12eq  39748  ax12el  39749  ax12inda  39755  ax12v2-o  39756  osumcllem8N  40770  pexmidlem5N  40781  mapdrvallem2  42452  sn-sup2  43298  onexomgt  44001  onexoegt  44004  omabs2  44092  clcnvlem  44382  onfrALT  45291  chordthmALT  45674  relpmin  45694  relpfrlem  45695  modelaxreplem1  45720  wfac8prim  45744  snelmap  45835  ssnnf1octb  45945  choicefi  45950  mapss2  45955  difmap  45956  axccdom  45971  infxrlesupxr  46183  inficc  46283  fsumnncl  46321  stoweidlem43  46790  stoweidlem48  46795  stoweidlem57  46804  stoweidlem60  46807  qndenserrnopn  47045  issalnnd  47092  subsaliuncl  47105  sge0cl  47128  nnfoctbdj  47203  ismeannd  47214  caragenunicl  47271  isomennd  47278  ovn0lem  47312  ovnsubaddlem2  47318  hspdifhsp  47363  hspmbllem3  47375  smflimlem6  47523  smfpimbor1lem1  47545  smfpimcc  47555  smfsuplem2  47559  rlimdmafv  47947  dfatcolem  48025  rlimdmafv2  48028  grimuhgr  48685  grimcnv  48686  grimco  48687  uhgrimedgi  48688  isuspgrim0  48692  gricushgr  48715  gricsym  48719  uhgrimisgrgric  48729  clnbgrgrimlem  48731  clnbgrgrim  48732  grimedg  48733  grtriprop  48739  usgrgrtrirex  48748  isubgr3stgrlem3  48766  uspgrlim  48790  grlimprclnbgredg  48795  grlimgredgex  48798  grlimgrtri  48801  xpco2  49668  opnneilv  49720  thincciso  50264