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

Theorem exlimdv 1848
 Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2067. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1875, ax-7 1922. (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 1833 . 2 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3 ax5e 1829 . 2 (∃𝑥𝜒𝜒)
42, 3syl6 34 1 (𝜑 → (∃𝑥𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  exlimdvv  1849  exlimddv  1850  ax13lem1  2236  ax13  2237  nfeqf  2289  axc15  2291  ax12v2OLD  2330  sbcom2  2433  tpid3gOLD  4249  sssn  4298  elpreqprb  4335  reusv2lem2  4795  reusv2lem2OLD  4796  ralxfr2d  4808  euotd  4900  wefrc  5032  wereu2  5035  releldmb  5281  relelrnb  5282  elres  5355  iss  5367  onfr  5680  dffv2  6181  dff3  6280  elunirn  6413  fsnex  6438  f1prex  6439  isomin  6487  isofrlem  6490  ovmpt4g  6681  soex  7002  f1oweALT  7043  op1steq  7101  fo2ndf  7171  mpt2xopynvov0g  7227  reldmtpos  7247  rntpos  7252  wfrlem12  7313  wfrlem17  7318  erdisj  7681  map0g  7783  resixpfo  7832  domdifsn  7928  xpdom3  7943  domunsncan  7945  enfixsn  7954  fodomr  7996  mapdom2  8016  mapdom3  8017  phplem4  8027  php3  8031  sucdom2  8041  pssnn  8063  ssfi  8065  domfi  8066  findcard2  8085  ac6sfi  8089  isfinite2  8103  xpfi  8116  domunfican  8118  fiint  8122  fodomfib  8125  mapfien2  8197  marypha1lem  8222  ordiso  8304  hartogslem1  8330  brwdom2  8361  wdomtr  8363  brwdom3  8370  unwdomg  8372  xpwdomg  8373  unxpwdom2  8376  inf3lem2  8409  epfrs  8490  tcmin  8500  cplem1  8635  pm54.43  8709  dfac8alem  8735  dfac8b  8737  dfac8clem  8738  ac10ct  8740  acni2  8752  acndom  8757  numwdom  8765  wdomfil  8767  wdomnumr  8770  iunfictbso  8820  dfac2  8836  dfac9  8841  kmlem13  8867  cdainf  8897  fictb  8950  cfeq0  8961  cff1  8963  cfflb  8964  cofsmo  8974  cfsmolem  8975  coftr  8978  infpssr  9013  fin4en1  9014  fin23lem7  9021  isf34lem4  9082  axcc3  9143  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  ac6num  9184  ttukeylem6  9219  ttukeyg  9222  fodomb  9229  iundom2g  9241  alephreg  9283  fpwwe2lem11  9341  fpwwe2lem12  9342  canthp1  9355  pwfseq  9365  gruen  9513  grudomon  9518  gruina  9519  grur1  9521  ltexnq  9676  ltbtwnnq  9679  genpn0  9704  psslinpr  9732  prlem934  9734  ltaddpr  9735  ltexprlem2  9738  ltexprlem6  9742  ltexprlem7  9743  reclem2pr  9749  reclem4pr  9751  suplem1pr  9753  negn0  10338  sup2  10858  supaddc  10867  supmul1  10869  zsupss  11653  fiinfnf1o  13000  hasheqf1oi  13002  hashfun  13084  hashf1  13098  rtrclreclem3  13648  rlimdm  14130  climcau  14249  caucvgb  14258  summolem2  14294  zsum  14296  sumz  14300  fsumf1o  14301  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumconst  14364  fsumrelem  14380  ntrivcvg  14468  prodmolem2  14504  zprod  14506  prod1  14513  fprodf1o  14515  fprodss  14517  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodconst  14547  fprodn0  14548  ruclem13  14810  4sqlem12  15498  vdwapun  15516  vdwlem9  15531  vdwlem10  15532  ramz  15567  ramub1  15570  firest  15916  mremre  16087  isacs2  16137  iscatd2  16165  sscfn1  16300  sscfn2  16301  gsumval2a  17102  symggen  17713  cyggex2  18121  gsumval3  18131  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  gsum2d2  18196  pgpfac1lem5  18301  ablfaclem3  18309  lss0cl  18768  lspsnat  18966  cnsubrg  19625  gsumfsum  19632  obslbs  19893  lmiclbs  19995  lmisfree  20000  mdetdiaglem  20223  mdet0  20231  eltg3  20577  tgtop  20588  tgidm  20595  ppttop  20621  toponmre  20707  tgrest  20773  neitr  20794  tgcn  20866  cmpsublem  21012  cmpsub  21013  iunconlem  21040  uncon  21042  1stcfb  21058  2ndcctbss  21068  2ndcdisj  21069  1stcelcls  21074  1stccnp  21075  locfincmp  21139  comppfsc  21145  1stckgen  21167  ptuni2  21189  ptbasfi  21194  ptpjopn  21225  ptclsg  21228  ptcnp  21235  prdstopn  21241  txindis  21247  txtube  21253  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  txcon  21302  trfbas2  21457  filtop  21469  filcon  21497  filssufilg  21525  fmfnfm  21572  ufldom  21576  hauspwpwf1  21601  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem2  21667  tmdgsum2  21710  tgptsmscld  21764  ustfilxp  21826  xbln0  22029  opnreen  22442  metdsre  22464  cnheibor  22562  phtpc01  22604  cfilfcls  22880  cmetcaulem  22894  iscmet3  22899  ovolctb  23065  ovoliunlem3  23079  ovoliunnul  23082  ovolicc2lem5  23096  ovolicc2  23097  dyadmbl  23174  vitali  23188  itg11  23264  bddmulibl  23411  perfdvf  23473  dvcnp2  23489  dvlip  23560  dvne0  23578  fta1g  23731  fta1  23867  ulmcau  23953  pserulm  23980  wilthlem2  24595  dchrvmasumif  24992  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  dchrmusum  25013  dchrvmasum  25014  axcontlem10  25653  upgredg  25811  usgrafisindb1  25938  wlkiswwlk  26226  wlklniswwlkn  26229  clwlkisclwwlklem0  26316  clwlkfoclwwlk  26372  frgra3vlem2  26528  spansncvi  27895  reff  29234  locfinreflem  29235  cmpcref  29245  fmcncfil  29305  volmeas  29621  omssubadd  29689  bnj849  30249  derangenlem  30407  cvmsss2  30510  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmliftlem15  30534  cvmlift2lem10  30548  cvmlift3lem8  30562  fundmpss  30910  frmin  30983  frrlem11  31036  nocvxmin  31090  fnessref  31522  refssfne  31523  neibastop2lem  31525  neibastop2  31526  fnemeet2  31532  fnejoin2  31534  tailfb  31542  knoppcnlem9  31661  wl-ax13lem1  32466  wl-sbcom2d  32523  matunitlindflem2  32576  poimirlem25  32604  poimirlem27  32606  heicant  32614  itg2addnclem  32631  sdclem1  32709  fdc  32711  istotbnd3  32740  sstotbnd2  32743  prdsbnd2  32764  heibor1lem  32778  heiborlem1  32780  heiborlem10  32789  heibor  32790  riscer  32957  divrngidl  32997  prtlem17  33179  ax12eq  33244  ax12el  33245  ax12inda  33251  ax12v2-o  33252  osumcllem8N  34267  pexmidlem5N  34278  mapdrvallem2  35952  clcnvlem  36949  onfrALT  37785  chordthmALT  38191  snelmap  38280  ssnnf1octb  38377  choicefi  38387  mapss2  38392  difmap  38394  axccdom  38411  inficc  38608  fsumnncl  38638  stoweidlem43  38936  stoweidlem48  38941  stoweidlem57  38950  stoweidlem60  38953  qndenserrnopn  39194  issalnnd  39239  subsaliuncl  39252  sge0cl  39274  nnfoctbdj  39349  ismeannd  39360  caragenunicl  39414  isomennd  39421  ovn0lem  39455  ovnsubaddlem2  39461  hspdifhsp  39506  hspmbllem3  39518  smflimlem6  39662  smfpimbor1lem1  39683  rlimdmafv  39906  usgr1v0e  40545  1wlkiswwlks  41073  1wlkiswwlkupgr  41075  1wlklnwwlkn  41081  1wlklnwwlknupgr  41083  umgrwwlks2on  41161  elwwlks2  41170  elwspths2spth  41171  clwlkclwwlklem3  41210  clwlksfoclwwlk  41270  frgr3vlem2  41444  mgmpropd  41565  c0snmgmhm  41704
 Copyright terms: Public domain W3C validator