Theorem exlimdv 1960

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

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

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

This theorem is referenced by:  exlimdvv  1961  exlimddv  1962  ax13lem1  2412  ax13  2413  nfeqf  2419  axc15  2460  sssn  4793  elpreqprb  4834  reusv2lem2  5368  ralxfr2d  5379  euotd  5494  wefrc  5653  wereu2  5656  releldmb  5934  relelrnb  5935  iss  6035  frpomin  6338  onfr  6397  dffv2  6974  dff3  7093  elunirn  7247  fsnex  7279  f1prex  7280  isomin  7333  isofrlem  7336  ovmpt4g  7555  soex  7914  f1oweALT  7965  op1steq  8026  fo2ndf  8112  frxp3  8143  mpoxopynvov0g  8206  reldmtpos  8226  rntpos  8231  frrlem10  8288  fprresex  8303  erdisj  8748  map0g  8878  resixpfo  8930  domdifsn  9044  xpdom3  9059  domunsncan  9061  enfixsn  9070  fodomr  9112  mapdom2  9132  mapdom3  9133  rexdif1en  9141  pssnn  9149  ssfiALT  9154  domfi  9169  sucdom2  9183  phplem2  9185  php3  9189  0sdom1dom  9202  sdom1  9206  1sdom2dom  9210  ac6sfi  9240  isfinite2  9254  domunfican  9277  fiint  9282  fodomfir  9283  fodomfib  9284  mapfien2  9365  marypha1lem  9389  ordiso  9474  hartogslem1  9500  brwdom2  9531  wdomtr  9533  brwdom3  9540  unwdomg  9542  xpwdomg  9543  unxpwdom2  9546  inf3lem2  9594  ttrclss  9685  dmttrcl  9686  rnttrcl  9687  ttrclselem2  9691  epfrs  9696  tcmin  9704  frmin  9717  cplem1  9871  pm54.43  9983  dfac8alem  10009  dfac8b  10011  dfac8clem  10012  ac10ct  10014  acni2  10026  acndom  10031  numwdom  10039  wdomfil  10041  wdomnumr  10044  iunfictbso  10094  dfac2b  10110  dfac9  10116  kmlem13  10142  djuinf  10168  fictb  10223  cfeq0  10236  cff1  10238  cfflb  10239  cofsmo  10249  cfsmolem  10250  coftr  10253  infpssr  10288  fin4en1  10289  fin23lem7  10296  isf34lem4  10357  axcc3  10418  domtriomlem  10422  axdc2lem  10428  axdc3lem2  10431  axdc3lem4  10433  axdc4lem  10435  ac6num  10459  ttukeylem6  10494  ttukeyg  10497  fodomb  10506  iundom2g  10520  alephreg  10563  fpwwe2lem10  10621  fpwwe2lem11  10622  canthp1  10635  pwfseq  10645  gruen  10793  grudomon  10798  gruina  10799  grur1  10801  ltexnq  10956  ltbtwnnq  10959  genpn0  10984  psslinpr  11012  prlem934  11014  ltaddpr  11015  ltexprlem2  11018  ltexprlem6  11022  ltexprlem7  11023  reclem2pr  11029  reclem4pr  11031  suplem1pr  11033  negn0  11639  sup2  12167  supaddc  12178  supmul1  12180  zsupss  12957  fiinfnf1o  14382  hasheqf1oi  14383  hashfun  14470  hashf1  14490  hash3tpexb  14527  rtrclreclem3  15093  rlimdm  15598  climcau  15718  caucvgb  15727  summolem2  15763  zsum  15765  sumz  15769  fsumf1o  15770  fsumss  15772  fsumcl2lem  15778  fsumadd  15787  fsummulc2  15831  fsumconst  15837  fsumrelem  15855  ntrivcvg  15947  prodmolem2  15985  zprod  15987  prod1  15994  fprodf1o  15996  fprodss  15998  fprodcl2lem  16000  fprodmul  16010  fproddiv  16011  fprodconst  16028  fprodn0  16029  ruclem13  16294  4sqlem12  17012  vdwapun  17030  vdwlem9  17045  vdwlem10  17046  ramz  17081  ramub1  17084  firest  17481  mremre  17652  isacs2  17705  iscatd2  17733  cicsym  17857  sscfn1  17870  sscfn2  17871  initoeu2  18069  mgmpropd  18705  gsumval2a  18739  symggen  19536  cyggex2  19963  gsumval3  19973  gsumzres  19975  gsumzcl2  19976  gsumzf1o  19978  gsumzaddlem  19987  gsumconst  20000  gsumzmhm  20003  gsumzoppg  20010  gsum2d2  20040  pgpfac1lem5  20147  ablfaclem3  20155  c0snmgmhm  20540  lss0cl  21042  lspsnat  21243  qsidomlem2  21446  cnsubrg  21542  gsumfsum  21549  obslbs  21845  lmiclbs  21952  lmisfree  21957  mdetdiaglem  22720  mdet0  22728  eltg3  23084  tgtop  23095  tgidm  23102  ppttop  23129  toponmre  23215  tgrest  23281  neitr  23302  tgcn  23374  cmpsublem  23521  cmpsub  23522  iunconnlem  23549  unconn  23551  1stcfb  23567  2ndcctbss  23577  2ndcdisj  23578  1stcelcls  23583  1stccnp  23584  locfincmp  23648  comppfsc  23654  1stckgen  23676  ptuni2  23698  ptbasfi  23703  ptpjopn  23734  ptclsg  23737  ptcnp  23744  prdstopn  23750  txindis  23756  txtube  23762  txcmplem1  23763  txcmplem2  23764  xkococnlem  23781  txconn  23811  trfbas2  23965  filtop  23977  filconn  24005  filssufilg  24033  fmfnfm  24080  ufldom  24084  hauspwpwf1  24109  alexsubALTlem3  24171  alexsubALT  24173  ptcmplem2  24175  tmdgsum2  24218  tgptsmscld  24273  ustfilxp  24335  xbln0  24536  opnreen  24954  metdsre  24976  cnheibor  25079  phtpc01  25120  cfilfcls  25398  cmetcaulem  25412  iscmet3  25417  ovolctb  25614  ovoliunlem3  25628  ovoliunnul  25631  ovolicc2lem5  25645  ovolicc2  25646  dyadmbl  25724  vitali  25737  itg11  25815  bddmulibl  25963  perfdvf  26027  dvcnp2  26044  dvlip  26117  dvne0  26135  fta1g  26292  fta1  26434  ulmcau  26520  pserulm  26547  wilthlem2  27195  dchrvmasumif  27629  rpvmasum2  27638  dchrisum0re  27639  dchrisum0lem3  27645  dchrisum0  27646  dchrmusum  27650  dchrvmasum  27651  noinfno  27844  nobdaymin  27908  ltslpss  28063  axcontlem10  29260  usgr1v0e  29613  wlkiswwlks  30162  wlkiswwlkupgr  30164  wlklnwwlkn  30170  wlklnwwlknupgr  30172  usgrwwlks2on  30244  umgrwwlks2on  30245  elwwlks2  30255  elwspths2spth  30256  clwlkclwwlklem3  30289  clwlkclwwlkfo  30297  frgr3vlem2  30562  spansncvi  31941  2ndresdju  32931  fnpreimac  32952  gsumwrd2dccatlem  33334  reff  34170  locfinreflem  34171  cmpcref  34181  fmcncfil  34262  volmeas  34562  omssubadd  34631  bnj849  35254  r1filimi  35435  onvfowev  35495  acycgrislfgr  35539  derangenlem  35558  cvmsss2  35661  cvmopnlem  35665  cvmfolem  35666  cvmliftmolem2  35669  cvmliftlem15  35685  cvmlift2lem10  35699  cvmlift3lem8  35713  satfdmlem  35755  sat1el2xp  35766  fmlasuc  35773  fundmpss  36154  fnessref  36753  refssfne  36754  neibastop2lem  36756  neibastop2  36757  fnemeet2  36763  fnejoin2  36765  tailfb  36773  axuntco  36875  dfttc4lem2  36925  knoppcnlem9  36975  isinf2  37934  pibt2  37946  wl-ax13lem1  38023  wl-sbcom2d  38099  matunitlindflem2  38151  poimirlem25  38179  poimirlem27  38181  heicant  38189  itg2addnclem  38205  sdclem1  38277  fdc  38279  istotbnd3  38305  sstotbnd2  38308  prdsbnd2  38329  heibor1lem  38343  heiborlem1  38345  heiborlem10  38354  heibor  38355  riscer  38522  divrngidl  38562  iss2  38878  eqvreldisj  39232  disjlem17  39436  prtlem17  39535  ax12eq  39600  ax12el  39601  ax12inda  39607  ax12v2-o  39608  osumcllem8N  40622  pexmidlem5N  40633  mapdrvallem2  42304  sn-sup2  43148  onexomgt  43853  onexoegt  43856  omabs2  43944  clcnvlem  44234  onfrALT  45143  chordthmALT  45526  relpmin  45546  relpfrlem  45547  modelaxreplem1  45572  wfac8prim  45596  snelmap  45687  ssnnf1octb  45797  choicefi  45802  mapss2  45807  difmap  45808  axccdom  45823  infxrlesupxr  46035  inficc  46135  fsumnncl  46173  stoweidlem43  46642  stoweidlem48  46647  stoweidlem57  46656  stoweidlem60  46659  qndenserrnopn  46897  issalnnd  46944  subsaliuncl  46957  sge0cl  46980  nnfoctbdj  47055  ismeannd  47066  caragenunicl  47123  isomennd  47130  ovn0lem  47164  ovnsubaddlem2  47170  hspdifhsp  47215  hspmbllem3  47227  smflimlem6  47375  smfpimbor1lem1  47397  smfpimcc  47407  smfsuplem2  47411  rlimdmafv  47796  dfatcolem  47874  rlimdmafv2  47877  grimuhgr  48534  grimcnv  48535  grimco  48536  uhgrimedgi  48537  isuspgrim0  48541  gricushgr  48564  gricsym  48568  uhgrimisgrgric  48578  clnbgrgrimlem  48580  clnbgrgrim  48581  grimedg  48582  grtriprop  48588  usgrgrtrirex  48597  isubgr3stgrlem3  48615  uspgrlim  48639  grlimprclnbgredg  48644  grlimgredgex  48647  grlimgrtri  48650  xpco2  49513  opnneilv  49565  thincciso  50109