Theorem exlimdv 1965

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  exlimdvv  1966  exlimddv  1967  ax13lem1  2403  ax13  2404  nfeqf  2410  axc15  2451  sssn  4781  elpreqprb  4822  reusv2lem2  5360  ralxfr2d  5371  euotd  5485  wefrc  5644  wereu2  5647  releldmb  5927  relelrnb  5928  iss  6026  frpomin  6343  onfr  6402  dffv2  6981  dff3  7101  elunirn  7256  fsnex  7292  f1prex  7293  isomin  7346  isofrlem  7349  ovmpt4g  7568  soex  7934  f1oweALT  7985  op1steq  8046  fo2ndf  8135  frxp3  8171  mpoxopynvov0g  8235  reldmtpos  8255  rntpos  8260  frrlem10  8317  fprresex  8332  erdisj  8779  map0g  8916  resixpfo  8968  domdifsn  9083  xpdom3  9098  domunsncan  9100  enfixsn  9109  fodomr  9151  mapdom2  9171  mapdom3  9172  rexdif1en  9180  pssnn  9188  ssfiALT  9193  domfi  9208  sucdom2  9222  phplem2  9224  php3  9228  0sdom1dom  9241  sdom1  9245  1sdom2dom  9249  ac6sfi  9279  isfinite2  9294  domunfican  9317  fiint  9322  fodomfir  9323  fodomfib  9324  mapfien2  9405  marypha1lem  9429  ordiso  9514  hartogslem1  9540  brwdom2  9571  wdomtr  9573  brwdom3  9580  unwdomg  9582  xpwdomg  9583  unxpwdom2  9586  inf3lem2  9634  ttrclss  9725  dmttrcl  9726  rnttrcl  9727  ttrclselem2  9731  epfrs  9736  tcmin  9744  frmin  9757  r1filimi  9907  cplem1  9954  cplem1OLD  9955  karden  9963  pm54.43  10086  dfac8alem  10112  dfac8b  10114  dfac8clem  10115  ac10ct  10117  acni2  10129  acndom  10134  numwdom  10142  wdomfil  10144  wdomnumr  10147  iunfictbso  10197  dfac2b  10213  dfac9  10219  kmlem13  10245  djuinf  10271  fictb  10326  cfeq0  10338  cff1  10340  cfflb  10341  cofsmo  10351  cfsmolem  10352  coftr  10355  infpssr  10390  fin4en1  10391  fin23lem7  10398  isf34lem4  10459  axcc3  10520  domtriomlem  10524  axdc2lem  10530  axdc3lem2  10533  axdc3lem4  10535  axdc4lem  10537  ac6num  10561  ttukeylem6  10596  ttukeyg  10599  fodomb  10609  iundom2g  10628  alephreg  10671  fpwwe2lem10  10729  fpwwe2lem11  10730  canthp1  10743  pwfseq  10753  gruen  10901  grudomon  10906  gruina  10907  grur1  10909  ltexnq  11064  ltbtwnnq  11067  genpn0  11092  psslinpr  11120  prlem934  11122  ltaddpr  11123  ltexprlem2  11126  ltexprlem6  11130  ltexprlem7  11131  reclem2pr  11137  reclem4pr  11139  suplem1pr  11141  negn0  11749  sup2  12277  supaddc  12288  supmul1  12290  zsupss  13068  fiinfnf1o  14498  hasheqf1oi  14499  hashfun  14586  hashf1  14606  hash3tpexb  14643  rtrclreclem3  15219  rlimdm  15724  climcau  15844  caucvgb  15853  summolem2  15888  zsum  15890  sumz  15894  fsumf1o  15895  fsumss  15897  fsumcl2lem  15903  fsumadd  15912  fsummulc2  15956  fsumconst  15962  fsumrelem  15980  ntrivcvg  16072  prodmolem2  16108  zprod  16110  prod1  16117  fprodf1o  16119  fprodss  16121  fprodcl2lem  16123  fprodmul  16133  fproddiv  16134  fprodconst  16151  fprodn0  16152  ruclem13  16416  4sqlem12  17140  vdwapun  17158  vdwlem9  17173  vdwlem10  17174  ramz  17209  ramub1  17212  firest  17609  mremre  17780  isacs2  17833  iscatd2  17861  cicsym  17985  sscfn1  17998  sscfn2  17999  initoeu2  18197  mgmpropd  18835  gsumval2a  18880  symggen  19690  cyggex2  20117  gsumval3  20127  gsumzres  20129  gsumzcl2  20130  gsumzf1o  20132  gsumzaddlem  20141  gsumconst  20154  gsumzmhm  20157  gsumzoppg  20164  gsum2d2  20194  pgpfac1lem5  20301  ablfaclem3  20309  c0snmgmhm  20698  lss0cl  21228  lspsnat  21429  qsidomlem2  21643  cnsubrg  21739  gsumfsum  21746  obslbs  22042  lmiclbs  22149  lmisfree  22154  mdetdiaglem  22919  mdet0  22927  matunitlindflem2  23001  eltg3  23286  tgtop  23297  tgidm  23304  ppttop  23331  toponmre  23417  tgrest  23483  neitr  23504  tgcn  23576  cmpsublem  23723  cmpsub  23724  iunconnlem  23751  unconn  23753  1stcfb  23769  2ndcctbss  23780  2ndcdisj  23781  1stcelcls  23786  1stccnp  23787  locfincmp  23851  comppfsc  23857  1stckgen  23879  ptuni2  23901  ptbasfi  23906  ptpjopn  23937  ptclsg  23940  ptcnp  23947  prdstopn  23953  txindis  23959  txtube  23965  txcmplem1  23966  txcmplem2  23967  xkococnlem  23984  txconn  24014  trfbas2  24168  filtop  24180  filconn  24208  filssufilg  24236  fmfnfm  24283  ufldom  24287  hauspwpwf1  24312  alexsubALTlem3  24374  alexsubALT  24376  ptcmplem2  24378  tmdgsum2  24421  tgptsmscld  24476  ustfilxp  24538  xbln0  24739  opnreen  25157  metdsre  25179  cnheibor  25282  phtpc01  25323  cfilfcls  25601  cmetcaulem  25615  iscmet3  25620  ovolctb  25817  ovoliunlem3  25831  ovoliunnul  25834  ovolicc2lem5  25848  ovolicc2  25849  dyadmbl  25927  vitali  25940  itg11  26018  bddmulibl  26165  perfdvf  26229  dvcnp2  26246  dvlip  26319  dvne0  26337  fta1g  26494  fta1  26635  ulmcau  26728  pserulm  26755  wilthlem2  27402  dchrvmasumif  27836  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lem3  27852  dchrisum0  27853  dchrmusum  27857  dchrvmasum  27858  noinfno  28081  nobdaymin  28145  ltslpss  28300  axcontlem10  29557  usgr1v0e  29913  wlkiswwlks  30471  wlkiswwlkupgr  30473  wlklnwwlkn  30479  wlklnwwlknupgr  30481  usgrwwlks2on  30553  umgrwwlks2on  30554  elwwlks2  30564  elwspths2spth  30565  clwlkclwwlklem3  30598  clwlkclwwlkfo  30606  frgr3vlem2  30881  spansncvi  32260  2ndresdju  33291  fnpreimac  33312  gsumwrd2dccatlem  33685  reff  34518  locfinreflem  34519  cmpcref  34529  fmcncfil  34610  volmeas  34911  bnj849  35602  soinfdom  35769  weexenwe  35813  acwer1prc  35817  kardfi  35895  onvfowev  35970  acycgrislfgr  35994  derangenlem  36023  cvmsss2  36126  cvmopnlem  36130  cvmfolem  36131  cvmliftmolem2  36134  cvmliftlem15  36150  cvmlift2lem10  36164  cvmlift3lem8  36178  satfdmlem  36220  sat1el2xp  36231  fmlasuc  36238  fundmpss  36625  fnessref  37238  refssfne  37239  neibastop2lem  37241  neibastop2  37242  fnemeet2  37248  fnejoin2  37250  tailfb  37258  axuntco  37360  dfttc4lem2  37410  knoppcnlem9  37460  isinf2  38422  pibt2  38434  wl-ax13lem1  38511  wl-sbcom2d  38587  poimirlem25  38657  poimirlem27  38659  heicant  38667  itg2addnclem  38683  sdclem1  38771  fdc  38773  istotbnd3  38799  sstotbnd2  38802  prdsbnd2  38823  heibor1lem  38837  heiborlem1  38839  heiborlem10  38848  heibor  38849  riscer  39016  divrngidl  39056  iss2  39370  eqvreldisj  39724  disjlem17  39928  prtlem17  40027  ax12eq  40092  ax12el  40093  ax12inda  40099  ax12v2-o  40100  osumcllem8N  41114  pexmidlem5N  41125  mapdrvallem2  42796  sn-sup2  43649  onexomgt  44337  onexoegt  44340  omabs2  44428  clcnvlem  44717  onfrALT  45626  chordthmALT  46009  cocanss2  46016  relpmin  46036  relpfrlem  46037  modelaxreplem1  46062  wfac8prim  46086  snelmap  46193  ssnnf1octb  46303  choicefi  46308  mapss2  46313  difmap  46314  axccdom  46329  infxrlesupxr  46540  inficc  46640  fsumnncl  46678  stoweidlem43  47147  stoweidlem48  47152  stoweidlem57  47161  stoweidlem60  47164  qndenserrnopn  47402  issalnnd  47449  subsaliuncl  47462  sge0cl  47485  nnfoctbdj  47560  ismeannd  47571  caragenunicl  47628  isomennd  47635  ovn0lem  47669  ovnsubaddlem2  47675  hspdifhsp  47720  hspmbllem3  47732  smflimlem6  47880  smfpimbor1lem1  47902  smfpimcc  47912  smfsuplem2  47916  rlimdmafv  48341  dfatcolem  48419  rlimdmafv2  48422  grimuhgr  49079  grimcnv  49080  grimco  49081  uhgrimedgi  49082  isuspgrim0  49086  gricushgr  49109  gricsym  49113  uhgrimisgrgric  49123  clnbgrgrimlem  49125  clnbgrgrim  49126  grimedg  49127  grtriprop  49133  usgrgrtrirex  49142  isubgr3stgrlem3  49160  uspgrlim  49184  grlimprclnbgredg  49189  grlimgredgex  49192  grlimgrtri  49195  xpco2  50062  opnneilv  50117  thincciso  50682