MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimdv Structured version   Visualization version   GIF version

Theorem exlimdv 1901
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2118. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1945, ax-7 1981. (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
StepHypRef Expression
1 exlimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21eximdv 1886 . 2 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3 ax5e 1881 . 2 (∃𝑥𝜒𝜒)
42, 3syl6 35 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  exlimdvv  1902  exlimddv  1903  ax13lem1  2284  ax13  2285  nfeqf  2337  axc15  2339  sbcom2  2473  sssn  4390  elpreqprb  4428  reusv2lem2  4899  reusv2lem2OLD  4900  ralxfr2d  4912  euotd  5004  wefrc  5137  wereu2  5140  releldmb  5392  relelrnb  5393  elres  5470  iss  5482  onfr  5801  dffv2  6310  dff3  6412  elunirn  6549  fsnex  6578  f1prex  6579  isomin  6627  isofrlem  6630  ovmpt4g  6825  soex  7151  f1oweALT  7194  op1steq  7254  fo2ndf  7329  mpt2xopynvov0g  7385  reldmtpos  7405  rntpos  7410  wfrlem12  7471  wfrlem17  7476  erdisj  7837  map0g  7939  resixpfo  7988  domdifsn  8084  xpdom3  8099  domunsncan  8101  enfixsn  8110  fodomr  8152  mapdom2  8172  mapdom3  8173  phplem4  8183  php3  8187  sucdom2  8197  pssnn  8219  ssfi  8221  domfi  8222  findcard2  8241  ac6sfi  8245  isfinite2  8259  xpfi  8272  domunfican  8274  fiint  8278  fodomfib  8281  mapfien2  8355  marypha1lem  8380  ordiso  8462  hartogslem1  8488  brwdom2  8519  wdomtr  8521  brwdom3  8528  unwdomg  8530  xpwdomg  8531  unxpwdom2  8534  inf3lem2  8564  epfrs  8645  tcmin  8655  cplem1  8790  pm54.43  8864  dfac8alem  8890  dfac8b  8892  dfac8clem  8893  ac10ct  8895  acni2  8907  acndom  8912  numwdom  8920  wdomfil  8922  wdomnumr  8925  iunfictbso  8975  dfac2  8991  dfac9  8996  kmlem13  9022  cdainf  9052  fictb  9105  cfeq0  9116  cff1  9118  cfflb  9119  cofsmo  9129  cfsmolem  9130  coftr  9133  infpssr  9168  fin4en1  9169  fin23lem7  9176  isf34lem4  9237  axcc3  9298  domtriomlem  9302  axdc2lem  9308  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  ac6num  9339  ttukeylem6  9374  ttukeyg  9377  fodomb  9386  iundom2g  9400  alephreg  9442  fpwwe2lem11  9500  fpwwe2lem12  9501  canthp1  9514  pwfseq  9524  gruen  9672  grudomon  9677  gruina  9678  grur1  9680  ltexnq  9835  ltbtwnnq  9838  genpn0  9863  psslinpr  9891  prlem934  9893  ltaddpr  9894  ltexprlem2  9897  ltexprlem6  9901  ltexprlem7  9902  reclem2pr  9908  reclem4pr  9910  suplem1pr  9912  negn0  10497  sup2  11017  supaddc  11028  supmul1  11030  zsupss  11815  fiinfnf1o  13178  hasheqf1oi  13180  hashfun  13262  hashf1  13279  rtrclreclem3  13844  rlimdm  14326  climcau  14445  caucvgb  14454  summolem2  14491  zsum  14493  sumz  14497  fsumf1o  14498  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumconst  14566  fsumrelem  14583  ntrivcvg  14673  prodmolem2  14709  zprod  14711  prod1  14718  fprodf1o  14720  fprodss  14722  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodconst  14752  fprodn0  14753  ruclem13  15015  4sqlem12  15707  vdwapun  15725  vdwlem9  15740  vdwlem10  15741  ramz  15776  ramub1  15779  firest  16140  mremre  16311  isacs2  16361  iscatd2  16389  sscfn1  16524  sscfn2  16525  gsumval2a  17326  symggen  17936  cyggex2  18344  gsumval3  18354  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  gsum2d2  18419  pgpfac1lem5  18524  ablfaclem3  18532  lss0cl  18995  lspsnat  19193  cnsubrg  19854  gsumfsum  19861  obslbs  20122  lmiclbs  20224  lmisfree  20229  mdetdiaglem  20452  mdet0  20460  eltg3  20814  tgtop  20825  tgidm  20832  ppttop  20859  toponmre  20945  tgrest  21011  neitr  21032  tgcn  21104  cmpsublem  21250  cmpsub  21251  iunconnlem  21278  unconn  21280  1stcfb  21296  2ndcctbss  21306  2ndcdisj  21307  1stcelcls  21312  1stccnp  21313  locfincmp  21377  comppfsc  21383  1stckgen  21405  ptuni2  21427  ptbasfi  21432  ptpjopn  21463  ptclsg  21466  ptcnp  21473  prdstopn  21479  txindis  21485  txtube  21491  txcmplem1  21492  txcmplem2  21493  xkococnlem  21510  txconn  21540  trfbas2  21694  filtop  21706  filconn  21734  filssufilg  21762  fmfnfm  21809  ufldom  21813  hauspwpwf1  21838  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem2  21904  tmdgsum2  21947  tgptsmscld  22001  ustfilxp  22063  xbln0  22266  opnreen  22681  metdsre  22703  cnheibor  22801  phtpc01  22842  cfilfcls  23118  cmetcaulem  23132  iscmet3  23137  ovolctb  23304  ovoliunlem3  23318  ovoliunnul  23321  ovolicc2lem5  23335  ovolicc2  23336  dyadmbl  23414  vitali  23427  itg11  23503  bddmulibl  23650  perfdvf  23712  dvcnp2  23728  dvlip  23801  dvne0  23819  fta1g  23972  fta1  24108  ulmcau  24194  pserulm  24221  wilthlem2  24840  dchrvmasumif  25237  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem3  25253  dchrisum0  25254  dchrmusum  25258  dchrvmasum  25259  axcontlem10  25898  usgr1v0e  26263  wlkiswwlks  26830  wlkiswwlkupgr  26832  wlklnwwlkn  26838  wlklnwwlknupgr  26840  umgrwwlks2on  26923  elwwlks2  26933  elwspths2spth  26934  clwlkclwwlklem3  26967  clwlksfoclwwlk  27050  frgr3vlem2  27254  spansncvi  28639  reff  30034  locfinreflem  30035  cmpcref  30045  fmcncfil  30105  volmeas  30422  omssubadd  30490  bnj849  31121  derangenlem  31279  cvmsss2  31382  cvmopnlem  31386  cvmfolem  31387  cvmliftmolem2  31390  cvmliftlem15  31406  cvmlift2lem10  31420  cvmlift3lem8  31434  fundmpss  31790  frpomin  31863  frmin  31867  frrlem11  31917  nocvxmin  32019  fnessref  32477  refssfne  32478  neibastop2lem  32480  neibastop2  32481  fnemeet2  32487  fnejoin2  32489  tailfb  32497  knoppcnlem9  32616  wl-ax13lem1  33417  wl-sbcom2d  33474  matunitlindflem2  33536  poimirlem25  33564  poimirlem27  33566  heicant  33574  itg2addnclem  33591  sdclem1  33669  fdc  33671  istotbnd3  33700  sstotbnd2  33703  prdsbnd2  33724  heibor1lem  33738  heiborlem1  33740  heiborlem10  33749  heibor  33750  riscer  33917  divrngidl  33957  iss2  34252  prtlem17  34480  ax12eq  34545  ax12el  34546  ax12inda  34552  ax12v2-o  34553  osumcllem8N  35567  pexmidlem5N  35578  mapdrvallem2  37251  clcnvlem  38247  onfrALT  39081  chordthmALT  39483  snelmap  39568  ssnnf1octb  39696  choicefi  39706  mapss2  39711  difmap  39713  axccdom  39730  infxrlesupxr  39976  inficc  40079  fsumnncl  40121  stoweidlem43  40578  stoweidlem48  40583  stoweidlem57  40592  stoweidlem60  40595  qndenserrnopn  40836  issalnnd  40881  subsaliuncl  40894  sge0cl  40916  nnfoctbdj  40991  ismeannd  41002  caragenunicl  41059  isomennd  41066  ovn0lem  41100  ovnsubaddlem2  41106  hspdifhsp  41151  hspmbllem3  41163  smflimlem6  41305  smfpimbor1lem1  41326  smfpimcc  41335  smfsuplem2  41339  rlimdmafv  41578  mgmpropd  42100  c0snmgmhm  42239
  Copyright terms: Public domain W3C validator