Theorem exlimdv 1968

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2251. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 2002, ax-7 2043. (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 1952	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1947	. 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 1945

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

This theorem is used by:  exlimdvv  1969  exlimddv  1970  ax13lem1  2406  ax13  2407  nfeqf  2413  axc15  2454  sssn  4787  elpreqprb  4828  reusv2lem2  5368  ralxfr2d  5379  euotd  5493  wefrc  5652  wereu2  5655  releldmb  5940  relelrnb  5941  iss  6045  coass  6290  frpomin  6369  onfr  6428  dffv2  7011  dff3  7132  elunirn  7286  fsnex  7322  f1prex  7323  isomin  7376  isofrlem  7379  ovmpt4g  7599  soex  7967  f1oweALT  8018  op1steq  8079  fo2ndf  8169  frxp3  8205  mpoxopynvov0g  8269  reldmtpos  8289  rntpos  8294  frrlem10  8351  fprresex  8366  erdisj  8813  map0g  8950  resixpfo  9002  domdifsn  9117  xpdom3  9132  domunsncan  9134  enfixsn  9143  fodomr  9185  mapdom2  9205  mapdom3  9206  rexdif1en  9214  pssnn  9222  ssfiALT  9227  domfi  9242  sucdom2  9256  phplem2  9258  php3  9262  0sdom1dom  9275  sdom1  9279  1sdom2dom  9283  ac6sfi  9313  isfinite2  9328  domunfican  9351  fiint  9356  fodomfir  9357  fodomfib  9358  mapfien2  9438  marypha1lem  9462  ordiso  9547  hartogslem1  9573  brwdom2  9604  wdomtr  9606  brwdom3  9613  unwdomg  9615  xpwdomg  9616  unxpwdom2  9619  inf3lem2  9667  ttrclss  9758  dmttrcl  9759  rnttrcl  9760  ttrclselem2  9764  epfrs  9769  tcmin  9777  frmin  9790  r1filimi  9940  cplem1  9987  cplem1OLD  9988  karden  9996  pm54.43  10121  dfac8alem  10147  dfac8b  10149  dfac8clem  10150  ac10ct  10152  acni2  10164  acndom  10169  numwdom  10177  wdomfil  10179  wdomnumr  10182  iunfictbso  10232  dfac2b  10248  dfac9  10254  kmlem13  10280  djuinf  10306  fictb  10361  cfeq0  10373  cff1  10375  cfflb  10376  cofsmo  10386  cfsmolem  10387  coftr  10390  infpssr  10425  fin4en1  10426  fin23lem7  10433  isf34lem4  10494  axcc3  10555  domtriomlem  10559  axdc2lem  10565  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  ac6num  10596  ttukeylem6  10631  ttukeyg  10634  fodomb  10644  iundom2g  10663  alephreg  10706  fpwwe2lem10  10764  fpwwe2lem11  10765  canthp1  10778  pwfseq  10788  gruen  10936  grudomon  10941  gruina  10942  grur1  10944  ltexnq  11099  ltbtwnnq  11102  genpn0  11127  psslinpr  11155  prlem934  11157  ltaddpr  11158  ltexprlem2  11161  ltexprlem6  11165  ltexprlem7  11166  reclem2pr  11172  reclem4pr  11174  suplem1pr  11176  negn0  11784  sup2  12313  supaddc  12324  supmul1  12326  zsupss  13104  fiinfnf1o  14535  hasheqf1oi  14536  hashfun  14623  hashf1  14643  hash3tpexb  14680  rtrclreclem3  15256  rlimdm  15762  climcau  15882  caucvgb  15891  summolem2  15926  zsum  15928  sumz  15932  fsumf1o  15933  fsumss  15935  fsumcl2lem  15941  fsumadd  15950  fsummulc2  15994  fsumconst  16000  fsumrelem  16018  ntrivcvg  16110  prodmolem2  16146  zprod  16148  prod1  16155  fprodf1o  16157  fprodss  16159  fprodcl2lem  16161  fprodmul  16171  fproddiv  16172  fprodconst  16189  fprodn0  16190  ruclem13  16454  4sqlem12  17178  vdwapun  17196  vdwlem9  17211  vdwlem10  17212  ramz  17247  ramub1  17250  firest  17653  mremre  17824  isacs2  17877  iscatd2  17905  cicsym  18029  sscfn1  18042  sscfn2  18043  initoeu2  18241  mgmpropd  18879  gsumval2a  18924  symggen  19735  cyggex2  20162  gsumval3  20172  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumconst  20199  gsumzmhm  20202  gsumzoppg  20209  gsum2d2  20239  pgpfac1lem5  20346  ablfaclem3  20354  c0snmgmhm  20743  lss0cl  21273  lspsnat  21474  qsidomlem2  21688  cnsubrg  21787  gsumfsum  21794  obslbs  22091  lmiclbs  22198  lmisfree  22203  mdetdiaglem  22968  mdet0  22976  matunitlindflem2  23050  eltg3  23335  tgtop  23346  tgidm  23353  ppttop  23380  toponmre  23466  tgrest  23532  neitr  23553  tgcn  23625  cmpsublem  23772  cmpsub  23773  iunconnlem  23800  unconn  23802  1stcfb  23818  2ndcctbss  23829  2ndcdisj  23830  1stcelcls  23835  1stccnp  23836  locfincmp  23900  comppfsc  23906  1stckgen  23928  ptuni2  23950  ptbasfi  23955  ptpjopn  23986  ptclsg  23989  ptcnp  23996  prdstopn  24002  txindis  24008  txtube  24014  txcmplem1  24015  txcmplem2  24016  xkococnlem  24033  txconn  24063  trfbas2  24217  filtop  24229  filconn  24257  filssufilg  24285  fmfnfm  24332  ufldom  24336  hauspwpwf1  24361  alexsubALTlem3  24423  alexsubALT  24425  ptcmplem2  24427  tmdgsum2  24470  tgptsmscld  24525  ustfilxp  24587  xbln0  24788  opnreen  25206  metdsre  25228  cnheibor  25331  phtpc01  25372  cfilfcls  25650  cmetcaulem  25664  iscmet3  25669  ovolctb  25866  ovoliunlem3  25880  ovoliunnul  25883  ovolicc2lem5  25897  ovolicc2  25898  dyadmbl  25976  vitali  25989  itg11  26067  bddmulibl  26214  perfdvf  26278  dvcnp2  26295  dvlip  26368  dvne0  26386  fta1g  26543  fta1  26684  ulmcau  26779  pserulm  26806  wilthlem2  27453  dchrvmasumif  27887  rpvmasum2  27896  dchrisum0re  27897  dchrisum0lem3  27903  dchrisum0  27904  dchrmusum  27908  dchrvmasum  27909  noinfno  28132  nobdaymin  28196  ltslpss  28351  axcontlem10  29608  usgr1v0e  29964  wlkiswwlks  30522  wlkiswwlkupgr  30524  wlklnwwlkn  30530  wlklnwwlknupgr  30532  usgrwwlks2on  30604  umgrwwlks2on  30605  elwwlks2  30615  elwspths2spth  30616  clwlkclwwlklem3  30649  clwlkclwwlkfo  30657  frgr3vlem2  30932  spansncvi  32311  2ndresdju  33341  fnpreimac  33362  gsumwrd2dccatlem  33737  reff  34582  locfinreflem  34583  cmpcref  34593  fmcncfil  34674  volmeas  34975  bnj849  35666  soinfdom  35841  erscottd  35884  weexenwe  35889  acwer1prc  35893  kardfi  35979  onvfowev  36091  acycgrislfgr  36115  derangenlem  36144  cvmsss2  36247  cvmopnlem  36251  cvmfolem  36252  cvmliftmolem2  36255  cvmliftlem15  36271  cvmlift2lem10  36285  cvmlift3lem8  36299  satfdmlem  36341  sat1el2xp  36352  fmlasuc  36359  elpssmo  36673  fundmpss  36747  fnessref  37360  refssfne  37361  neibastop2lem  37363  neibastop2  37364  fnemeet2  37370  fnejoin2  37372  tailfb  37380  axuntco  37482  dfttc4lem2  37532  knoppcnlem9  37582  comodular  38207  isinf2  38596  pibt2  38608  wl-ax13lem1  38685  wl-sbcom2d  38761  poimirlem25  38831  poimirlem27  38833  heicant  38841  itg2addnclem  38857  sdclem1  38943  fdc  38945  istotbnd3  38971  sstotbnd2  38974  prdsbnd2  38995  heibor1lem  39009  heiborlem1  39011  heiborlem10  39020  heibor  39021  riscer  39188  divrngidl  39228  iss2  39542  eqvreldisj  39896  disjlem17  40100  prtlem17  40199  ax12eq  40264  ax12el  40265  ax12inda  40271  ax12v2-o  40272  osumcllem8N  41286  pexmidlem5N  41297  mapdrvallem2  42968  sn-sup2  43821  onexomgt  44504  onexoegt  44507  omabs2  44595  clcnvlem  44884  onfrALT  45792  chordthmALT  46175  cocanss2  46183  relpmin  46206  relpfrlem  46207  modelaxreplem1  46232  wfac8prim  46256  snelmap  46372  ssnnf1octb  46482  choicefi  46487  mapss2  46492  difmap  46493  axccdom  46508  infxrlesupxr  46719  inficc  46819  fsumnncl  46857  stoweidlem43  47326  stoweidlem48  47331  stoweidlem57  47340  stoweidlem60  47343  qndenserrnopn  47581  issalnnd  47628  subsaliuncl  47641  sge0cl  47664  nnfoctbdj  47739  ismeannd  47750  caragenunicl  47807  isomennd  47814  ovn0lem  47848  ovnsubaddlem2  47854  hspdifhsp  47899  hspmbllem3  47911  smflimlem6  48059  smfpimbor1lem1  48081  smfpimcc  48091  smfsuplem2  48095  rlimdmafv  48520  dfatcolem  48598  rlimdmafv2  48601  grimuhgr  49258  grimcnv  49259  grimco  49260  uhgrimedgi  49261  isuspgrim0  49265  gricushgr  49288  gricsym  49292  uhgrimisgrgric  49302  clnbgrgrimlem  49304  clnbgrgrim  49305  grimedg  49306  grtriprop  49312  usgrgrtrirex  49321  isubgr3stgrlem3  49339  uspgrlim  49363  grlimprclnbgredg  49368  grlimgredgex  49371  grlimgrtri  49374  xpco2  50299  opnneilv  50354  thincciso  50919