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

Theorem exlimdv 1847
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2066. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1874, ax-7 1921. (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 1832 . 2 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3 ax5e 1828 . 2 (∃𝑥𝜒𝜒)
42, 3syl6 34 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  exlimdvv  1848  exlimddv  1849  ax13lem1  2235  ax13  2236  nfeqf  2288  axc15  2290  ax12v2OLD  2329  sbcom2  2432  tpid3gOLD  4248  sssn  4295  elpreqprb  4330  reusv2lem2  4789  reusv2lem2OLD  4790  ralxfr2d  4802  euotd  4890  wefrc  5021  wereu2  5024  releldmb  5267  relelrnb  5268  elres  5341  iss  5353  onfr  5665  dffv2  6165  dff3  6264  elunirn  6390  fsnex  6415  f1prex  6416  isomin  6464  isofrlem  6467  ovmpt4g  6658  soex  6979  f1oweALT  7020  op1steq  7078  fo2ndf  7148  mpt2xopynvov0g  7204  reldmtpos  7224  rntpos  7229  wfrlem12  7290  wfrlem17  7295  erdisj  7658  map0g  7760  resixpfo  7809  domdifsn  7905  xpdom3  7920  domunsncan  7922  enfixsn  7931  fodomr  7973  mapdom2  7993  mapdom3  7994  phplem4  8004  php3  8008  sucdom2  8018  pssnn  8040  ssfi  8042  domfi  8043  findcard2  8062  ac6sfi  8066  isfinite2  8080  xpfi  8093  domunfican  8095  fiint  8099  fodomfib  8102  mapfien2  8174  marypha1lem  8199  ordiso  8281  hartogslem1  8307  brwdom2  8338  wdomtr  8340  brwdom3  8347  unwdomg  8349  xpwdomg  8350  unxpwdom2  8353  inf3lem2  8386  epfrs  8467  tcmin  8477  cplem1  8612  pm54.43  8686  dfac8alem  8712  dfac8b  8714  dfac8clem  8715  ac10ct  8717  acni2  8729  acndom  8734  numwdom  8742  wdomfil  8744  wdomnumr  8747  iunfictbso  8797  dfac2  8813  dfac9  8818  kmlem13  8844  cdainf  8874  fictb  8927  cfeq0  8938  cff1  8940  cfflb  8941  cofsmo  8951  cfsmolem  8952  coftr  8955  infpssr  8990  fin4en1  8991  fin23lem7  8998  isf34lem4  9059  axcc3  9120  domtriomlem  9124  axdc2lem  9130  axdc3lem2  9133  axdc3lem4  9135  axdc4lem  9137  ac6num  9161  ttukeylem6  9196  ttukeyg  9199  fodomb  9206  iundom2g  9218  alephreg  9260  fpwwe2lem11  9318  fpwwe2lem12  9319  canthp1  9332  pwfseq  9342  gruen  9490  grudomon  9495  gruina  9496  grur1  9498  ltexnq  9653  ltbtwnnq  9656  genpn0  9681  psslinpr  9709  prlem934  9711  ltaddpr  9712  ltexprlem2  9715  ltexprlem6  9719  ltexprlem7  9720  reclem2pr  9726  reclem4pr  9728  suplem1pr  9730  negn0  10310  sup2  10830  supaddc  10839  supmul1  10841  zsupss  11611  fiinfnf1o  12954  hasheqf1oi  12956  hashfun  13038  hashf1  13052  rtrclreclem3  13596  rlimdm  14078  climcau  14197  caucvgb  14206  summolem2  14242  zsum  14244  sumz  14248  fsumf1o  14249  fsumss  14251  fsumcl2lem  14257  fsumadd  14265  fsummulc2  14306  fsumconst  14312  fsumrelem  14328  ntrivcvg  14416  prodmolem2  14452  zprod  14454  prod1  14461  fprodf1o  14463  fprodss  14465  fprodcl2lem  14467  fprodmul  14477  fproddiv  14478  fprodconst  14495  fprodn0  14496  ruclem13  14758  4sqlem12  15446  vdwapun  15464  vdwlem9  15479  vdwlem10  15480  ramz  15515  ramub1  15518  firest  15864  mremre  16035  isacs2  16085  iscatd2  16113  sscfn1  16248  sscfn2  16249  gsumval2a  17050  symggen  17661  cyggex2  18069  gsumval3  18079  gsumzres  18081  gsumzcl2  18082  gsumzf1o  18084  gsumzaddlem  18092  gsumconst  18105  gsumzmhm  18108  gsumzoppg  18115  gsum2d2  18144  pgpfac1lem5  18249  ablfaclem3  18257  lss0cl  18716  lspsnat  18914  cnsubrg  19573  gsumfsum  19580  obslbs  19840  lmiclbs  19942  lmisfree  19947  mdetdiaglem  20170  mdet0  20178  eltg3  20524  tgtop  20535  tgidm  20542  ppttop  20568  toponmre  20654  tgrest  20720  neitr  20741  tgcn  20813  cmpsublem  20959  cmpsub  20960  iunconlem  20987  uncon  20989  1stcfb  21005  2ndcctbss  21015  2ndcdisj  21016  1stcelcls  21021  1stccnp  21022  locfincmp  21086  comppfsc  21092  1stckgen  21114  ptuni2  21136  ptbasfi  21141  ptpjopn  21172  ptclsg  21175  ptcnp  21182  prdstopn  21188  txindis  21194  txtube  21200  txcmplem1  21201  txcmplem2  21202  xkococnlem  21219  txcon  21249  trfbas2  21404  filtop  21416  filcon  21444  filssufilg  21472  fmfnfm  21519  ufldom  21523  hauspwpwf1  21548  alexsubALTlem3  21610  alexsubALT  21612  ptcmplem2  21614  tmdgsum2  21657  tgptsmscld  21711  ustfilxp  21773  xbln0  21976  opnreen  22389  metdsre  22411  cnheibor  22509  phtpc01  22551  cfilfcls  22824  cmetcaulem  22838  iscmet3  22843  ovolctb  23009  ovoliunlem3  23023  ovoliunnul  23026  ovolicc2lem5  23040  ovolicc2  23041  dyadmbl  23118  vitali  23132  itg11  23208  bddmulibl  23355  perfdvf  23417  dvcnp2  23433  dvlip  23504  dvne0  23522  fta1g  23675  fta1  23811  ulmcau  23897  pserulm  23924  wilthlem2  24539  dchrvmasumif  24936  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lem3  24952  dchrisum0  24953  dchrmusum  24957  dchrvmasum  24958  axcontlem10  25598  usgrafisindb1  25731  wlkiswwlk  26019  wlklniswwlkn  26022  clwlkisclwwlklem0  26109  clwlkfoclwwlk  26165  frgra3vlem2  26321  spansncvi  27688  reff  29027  locfinreflem  29028  cmpcref  29038  fmcncfil  29098  volmeas  29414  omssubadd  29482  bnj849  30042  derangenlem  30200  cvmsss2  30303  cvmopnlem  30307  cvmfolem  30308  cvmliftmolem2  30311  cvmliftlem15  30327  cvmlift2lem10  30341  cvmlift3lem8  30355  fundmpss  30703  frmin  30776  frrlem11  30829  nocvxmin  30883  fnessref  31315  refssfne  31316  neibastop2lem  31318  neibastop2  31319  fnemeet2  31325  fnejoin2  31327  tailfb  31335  knoppcnlem9  31454  wl-ax13lem1  32249  wl-sbcom2d  32306  matunitlindflem2  32359  poimirlem25  32387  poimirlem27  32389  heicant  32397  itg2addnclem  32414  sdclem1  32492  fdc  32494  istotbnd3  32523  sstotbnd2  32526  prdsbnd2  32547  heibor1lem  32561  heiborlem1  32563  heiborlem10  32572  heibor  32573  riscer  32740  divrngidl  32780  prtlem17  32962  ax12eq  33027  ax12el  33028  ax12inda  33034  ax12v2-o  33035  osumcllem8N  34050  pexmidlem5N  34061  mapdrvallem2  35735  clcnvlem  36732  onfrALT  37568  chordthmALT  37974  snelmap  38063  ssnnf1octb  38160  choicefi  38170  mapss2  38175  difmap  38177  axccdom  38194  inficc  38391  fsumnncl  38421  stoweidlem43  38719  stoweidlem48  38724  stoweidlem57  38733  stoweidlem60  38736  qndenserrnopn  38977  issalnnd  39022  subsaliuncl  39035  sge0cl  39057  nnfoctbdj  39132  ismeannd  39143  caragenunicl  39197  isomennd  39204  ovn0lem  39238  ovnsubaddlem2  39244  hspdifhsp  39289  hspmbllem3  39301  smflimlem6  39445  smfpimbor1lem1  39466  rlimdmafv  39690  upgredg  40351  usgr1v0e  40526  1wlkiswwlks  41054  1wlkiswwlkupgr  41056  1wlklnwwlkn  41062  1wlklnwwlknupgr  41064  umgrwwlks2on  41142  elwwlks2  41151  elwspths2spth  41152  clwlkclwwlklem3  41191  clwlksfoclwwlk  41251  frgr3vlem2  41425  mgmpropd  41546  c0snmgmhm  41685
  Copyright terms: Public domain W3C validator