Theorem exlimdv 1937

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  exlimdvv  1938  exlimddv  1939  ax13lem1  2374  ax13  2375  nfeqf  2381  axc15  2422  sssn  4830  elpreqprb  4869  reusv2lem2  5398  ralxfr2d  5409  euotd  5514  wefrc  5671  wereu2  5674  releldmb  5946  relelrnb  5947  iss  6036  frpomin  6342  onfr  6404  dffv2  6987  dff3  7102  elunirn  7250  fsnex  7281  f1prex  7282  isomin  7334  isofrlem  7337  ovmpt4g  7555  soex  7912  f1oweALT  7959  op1steq  8019  fo2ndf  8107  frxp3  8137  mpoxopynvov0g  8199  reldmtpos  8219  rntpos  8224  frrlem10  8280  fprresex  8295  wfrlem12OLD  8320  wfrlem17OLD  8325  erdisj  8755  map0g  8878  resixpfo  8930  domdifsn  9054  xpdom3  9070  domunsncan  9072  enfixsn  9081  sucdom2OLD  9082  fodomr  9128  mapdom2  9148  mapdom3  9149  rexdif1en  9158  pssnn  9168  ssfiALT  9174  domfi  9192  sucdom2  9206  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  0sdom1dom  9238  sdom1  9242  1sdom2dom  9247  pssnnOLD  9265  findcard2OLD  9284  ac6sfi  9287  isfinite2  9301  xpfiOLD  9318  domunfican  9320  fiint  9324  fodomfib  9326  mapfien2  9404  marypha1lem  9428  ordiso  9511  hartogslem1  9537  brwdom2  9568  wdomtr  9570  brwdom3  9577  unwdomg  9579  xpwdomg  9580  unxpwdom2  9583  inf3lem2  9624  ttrclss  9715  dmttrcl  9716  rnttrcl  9717  ttrclselem2  9721  epfrs  9726  tcmin  9736  frmin  9744  cplem1  9884  pm54.43  9996  dfac8alem  10024  dfac8b  10026  dfac8clem  10027  ac10ct  10029  acni2  10041  acndom  10046  numwdom  10054  wdomfil  10056  wdomnumr  10059  iunfictbso  10109  dfac2b  10125  dfac9  10131  kmlem13  10157  djuinf  10183  fictb  10240  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  10577  fpwwe2lem10  10635  fpwwe2lem11  10636  canthp1  10649  pwfseq  10659  gruen  10807  grudomon  10812  gruina  10813  grur1  10815  ltexnq  10970  ltbtwnnq  10973  genpn0  10998  psslinpr  11026  prlem934  11028  ltaddpr  11029  ltexprlem2  11032  ltexprlem6  11036  ltexprlem7  11037  reclem2pr  11043  reclem4pr  11045  suplem1pr  11047  negn0  11643  sup2  12170  supaddc  12181  supmul1  12183  zsupss  12921  fiinfnf1o  14310  hasheqf1oi  14311  hashfun  14397  hashf1  14418  rtrclreclem3  15007  rlimdm  15495  climcau  15617  caucvgb  15626  summolem2  15662  zsum  15664  sumz  15668  fsumf1o  15669  fsumss  15671  fsumcl2lem  15677  fsumadd  15686  fsummulc2  15730  fsumconst  15736  fsumrelem  15753  ntrivcvg  15843  prodmolem2  15879  zprod  15881  prod1  15888  fprodf1o  15890  fprodss  15892  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodconst  15922  fprodn0  15923  ruclem13  16185  4sqlem12  16889  vdwapun  16907  vdwlem9  16922  vdwlem10  16923  ramz  16958  ramub1  16961  firest  17378  mremre  17548  isacs2  17597  iscatd2  17625  cicsym  17751  sscfn1  17764  sscfn2  17765  initoeu2  17966  gsumval2a  18604  symggen  19338  cyggex2  19765  gsumval3  19775  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsumzoppg  19812  gsum2d2  19842  pgpfac1lem5  19949  ablfaclem3  19957  lss0cl  20557  lspsnat  20758  cnsubrg  21005  gsumfsum  21012  obslbs  21285  lmiclbs  21392  lmisfree  21397  mdetdiaglem  22100  mdet0  22108  eltg3  22465  tgtop  22476  tgidm  22483  ppttop  22510  toponmre  22597  tgrest  22663  neitr  22684  tgcn  22756  cmpsublem  22903  cmpsub  22904  iunconnlem  22931  unconn  22933  1stcfb  22949  2ndcctbss  22959  2ndcdisj  22960  1stcelcls  22965  1stccnp  22966  locfincmp  23030  comppfsc  23036  1stckgen  23058  ptuni2  23080  ptbasfi  23085  ptpjopn  23116  ptclsg  23119  ptcnp  23126  prdstopn  23132  txindis  23138  txtube  23144  txcmplem1  23145  txcmplem2  23146  xkococnlem  23163  txconn  23193  trfbas2  23347  filtop  23359  filconn  23387  filssufilg  23415  fmfnfm  23462  ufldom  23466  hauspwpwf1  23491  alexsubALTlem3  23553  alexsubALT  23555  ptcmplem2  23557  tmdgsum2  23600  tgptsmscld  23655  ustfilxp  23717  xbln0  23920  opnreen  24347  metdsre  24369  cnheibor  24471  phtpc01  24512  cfilfcls  24791  cmetcaulem  24805  iscmet3  24810  ovolctb  25007  ovoliunlem3  25021  ovoliunnul  25024  ovolicc2lem5  25038  ovolicc2  25039  dyadmbl  25117  vitali  25130  itg11  25208  bddmulibl  25356  perfdvf  25420  dvcnp2  25437  dvlip  25510  dvne0  25528  fta1g  25685  fta1  25821  ulmcau  25907  pserulm  25934  wilthlem2  26573  dchrvmasumif  27006  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem3  27022  dchrisum0  27023  dchrmusum  27027  dchrvmasum  27028  noinfno  27221  nocvxmin  27280  sltlpss  27402  axcontlem10  28262  usgr1v0e  28614  wlkiswwlks  29161  wlkiswwlkupgr  29163  wlklnwwlkn  29169  wlklnwwlknupgr  29171  umgrwwlks2on  29242  elwwlks2  29251  elwspths2spth  29252  clwlkclwwlklem3  29285  clwlkclwwlkfo  29293  frgr3vlem2  29558  spansncvi  30936  2ndresdju  31905  fnpreimac  31927  qsidomlem2  32603  reff  32850  locfinreflem  32851  cmpcref  32861  fmcncfil  32942  volmeas  33260  omssubadd  33330  bnj849  33967  acycgrislfgr  34174  derangenlem  34193  cvmsss2  34296  cvmopnlem  34300  cvmfolem  34301  cvmliftmolem2  34304  cvmliftlem15  34320  cvmlift2lem10  34334  cvmlift3lem8  34348  satfdmlem  34390  sat1el2xp  34401  fmlasuc  34408  fundmpss  34769  gg-dvcnp2  35205  fnessref  35290  refssfne  35291  neibastop2lem  35293  neibastop2  35294  fnemeet2  35300  fnejoin2  35302  tailfb  35310  knoppcnlem9  35425  isinf2  36334  pibt2  36346  wl-ax13lem1  36423  wl-sbcom2d  36474  matunitlindflem2  36533  poimirlem25  36561  poimirlem27  36563  heicant  36571  itg2addnclem  36587  sdclem1  36659  fdc  36661  istotbnd3  36687  sstotbnd2  36690  prdsbnd2  36711  heibor1lem  36725  heiborlem1  36727  heiborlem10  36736  heibor  36737  riscer  36904  divrngidl  36944  iss2  37261  eqvreldisj  37532  disjlem17  37717  prtlem17  37794  ax12eq  37859  ax12el  37860  ax12inda  37866  ax12v2-o  37867  osumcllem8N  38882  pexmidlem5N  38893  mapdrvallem2  40564  sn-sup2  41390  onexomgt  42038  onexoegt  42041  omabs2  42130  clcnvlem  42422  onfrALT  43358  chordthmALT  43742  snelmap  43819  ssnnf1octb  43941  choicefi  43947  mapss2  43952  difmap  43954  axccdom  43969  infxrlesupxr  44194  inficc  44295  fsumnncl  44336  stoweidlem43  44807  stoweidlem48  44812  stoweidlem57  44821  stoweidlem60  44824  qndenserrnopn  45062  issalnnd  45109  subsaliuncl  45122  sge0cl  45145  nnfoctbdj  45220  ismeannd  45231  caragenunicl  45288  isomennd  45295  ovn0lem  45329  ovnsubaddlem2  45335  hspdifhsp  45380  hspmbllem3  45392  smflimlem6  45540  smfpimbor1lem1  45562  smfpimcc  45572  smfsuplem2  45576  rlimdmafv  45933  dfatcolem  46011  rlimdmafv2  46014  isomushgr  46542  isomuspgr  46550  isomgrsym  46552  isomgrtr  46555  mgmpropd  46593  c0snmgmhm  46761  opnneilv  47589  thincciso  47717