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

Theorem simplbi 476
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi (𝜑𝜓)

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpi 206 . 2 (𝜑 → (𝜓𝜒))
32simpld 475 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  an3  867  3simpa  1056  xoror  1468  sbequ2  1879  reurex  3149  eqimss  3636  pssss  3680  eldifi  3710  elinel1  3777  ssunsn2  4327  pwssun  4980  sopo  5012  wefr  5064  opelxp1  5110  relop  5232  ssrelrn  5275  ordtr  5696  funmo  5863  funrel  5864  fnfun  5946  ffn  6002  f1f  6058  f1of1  6093  f1ofo  6101  isof1o  6527  eqopi  7147  1st2nd2  7150  reldmtpos  7305  swoer  7717  erdisj  7739  ecopover  7796  ecopoverOLD  7797  sdomdom  7927  mapfien  8257  inf3lemd  8468  cardprclem  8749  infxpenlem  8780  cardinfima  8864  dfac5lem4  8893  domtriomlem  9208  smobeth  9352  fpwwe2lem6  9401  fpwwe2lem7  9402  fpwwe2lem12  9407  fpwwe2lem13  9408  fpwwe2  9409  axrnegex  9927  axpre-sup  9934  zre  11325  nnssz  11341  ixxss1  12135  ixxss2  12136  ixxss12  12137  lbioo  12148  ubioo  12149  iccss2  12186  rge0ssre  12222  elfzuz  12280  uzdisj  12354  nn0disj  12396  0wrd0  13270  splfv1  13443  sqrlem6  13922  rlimf  14166  lo1f  14183  lo1dm  14184  o1f  14194  o1dm  14195  mertenslem2  14542  fprodge0  14649  divalglem9  15048  bitsinv2  15089  bitsf1ocnv  15090  gcdcllem1  15145  coprmproddvdslem  15300  prmnn  15312  prmuz2  15332  phimullem  15408  hashgcdlem  15417  1arith  15555  ramtlecl  15628  0ramcl  15651  firest  16014  acsmre  16234  posprs  16870  latpos  16971  clatpos  17031  dlatl  17116  pslem  17127  tsrlemax  17141  tsrps  17142  sgrpmgm  17210  mndsgrp  17220  grpmnd  17350  nsgsubg  17547  ghmgrp1  17583  ghmgrp2  17584  gimghm  17627  gagrp  17646  gaset  17647  psgneu  17847  efgredeu  18086  ablgrp  18119  cmnmnd  18129  cyggenod2  18208  cyggrp  18212  ablfac2  18409  crngring  18479  dvdsrcl  18570  unitcl  18580  brric2  18666  drngring  18675  subrgring  18704  subrgrcl  18706  srngrhm  18772  lmimlmhm  18983  lveclmod  19025  2idlcpbl  19153  qus1  19154  qusrhm  19156  lpirring  19171  nzrring  19180  domnnzr  19214  fldidom  19224  assalmod  19238  assaring  19239  assasca  19240  cygznlem1  19834  cygznlem3  19837  lbslinds  20091  gsummatr01lem1  20380  topontop  20641  tpstop  20654  clsval2  20764  mretopd  20806  neiptoptop  20845  perftop  20870  restfpw  20893  cntop1  20954  cntop2  20955  cnptop1  20956  cnptop2  20957  cnprcl  20959  t1ficld  21041  t0top  21043  t1top  21044  haustop  21045  regtop  21047  nrmtop  21050  cnrmtop  21051  pnrmnrm  21054  cmptop  21108  discmp  21111  tgcmp  21114  uncmp  21116  conndisj  21129  conntop  21130  1stctop  21156  llytop  21185  nllytop  21186  hmeocn  21473  filfbas  21562  ufilfil  21618  flimtop  21679  flimfil  21683  alexsublem  21758  ptcmplem3  21768  tsmsfbas  21841  tsmslem1  21842  tsmsgsum  21852  tsmssubm  21856  tsmsres  21857  tsmsf1o  21858  tsmsmhm  21859  tsmsadd  21860  tsmsxplem1  21866  tsmsxplem2  21867  tsmsxp  21868  tlmtmd  21900  tlmlmod  21902  tlmtrg  21903  tvctlm  21910  ressust  21978  uspreg  21988  ucncn  21999  neipcfilu  22010  cuspusp  22014  isxmet2d  22042  metxmet  22049  xmstps  22168  msxms  22169  xmsxmet  22171  msmet  22172  stdbdxmet  22230  nrgngp  22376  nlmngp  22391  nlmlmod  22392  nlmnrg  22393  nvcnlm  22410  nmoi  22442  nghmrcl1  22446  nghmrcl2  22447  nmhmrcl1  22461  nmhmrcl2  22462  qdensere  22483  xrge0gsumle  22544  xrge0tsms  22545  metds0  22561  metdstri  22562  metdsre  22564  metdseq0  22565  metdscnlem  22566  metnrmlem1a  22569  metnrmlem1  22570  icopnfcnv  22649  cvsclm  22834  cmetmet  22992  cmsms  23053  hlbn  23067  ovolicc2lem5  23196  mblss  23206  mbff  23300  mbfres  23317  mbfadd  23334  mbfsub  23335  i1fmbf  23348  mbfmul  23399  bddmulibl  23511  limcmpt  23553  c1liplem1  23663  c1lip2  23665  fta1glem1  23829  fta1glem2  23830  fta1g  23831  fta1b  23833  ply1pid  23843  aacn  23976  ulmf2  24042  logdmnrp  24287  logdmss  24288  logcnlem2  24289  logcnlem3  24290  logcnlem4  24291  logcnlem5  24292  logcn  24293  dvloglem  24294  logf1o2  24296  efopnlem1  24302  logtayl2  24308  cxpcn  24386  cxpcn3lem  24388  cxpcn3  24389  resqrtcn  24390  atandmneg  24533  atandmcj  24536  cosatan  24548  cosatanne0  24549  birthdaylem1  24578  areacl  24589  cxp2lim  24603  jensenlem2  24614  jensen  24615  sqff1o  24808  dvdsmulf1o  24820  lgsqrlem1  24971  lgsqrlem2  24972  lgsqrlem3  24973  lgsqrlem4  24974  lgseisenlem3  25002  chebbnd1  25061  chtppilim  25064  chpchtlim  25068  chpo1ub  25069  dchrmusumlema  25082  dchrvmasumiflem1  25090  dchrisum0lema  25103  dchrisum0lem2  25107  selberg3lem2  25147  pntrsumo1  25154  selbergsb  25164  pnt2  25202  tglineeltr  25426  axcontlem2  25745  axcontlem7  25750  axcontlem8  25751  uhgr0vb  25863  lfuhgr1v0e  26039  fusgrusgr  26102  nbupgruvtxres  26195  cusgrusgr  26202  trliswlk  26463  clwlkiswlk  26539  eupthistrl  26937  frgrusgr  26990  frgrwopreg  27044  ablogrpo  27250  bnnv  27571  hlobn  27593  hcauseq  27891  hlimseqi  27895  hlimveci  27896  shss  27916  sh0  27922  chsh  27930  lnopf  28567  bdopln  28569  hmopf  28582  lnfnf  28592  unopf1o  28624  elunop2  28721  elpjhmop  28893  stcltrlem1  28984  mdslle1i  29025  mdslle2i  29026  rabexgfGS  29188  ssnnssfz  29391  tospos  29443  ogrpgrp  29488  ogrpinvOLD  29500  xrge0tsmsd  29570  ofldfld  29595  ofldlt1  29598  ofldchr  29599  isarchiofld  29602  reofld  29625  rearchi  29627  creftop  29695  lmxrge0  29780  qqhrhm  29815  esumpcvgval  29921  dynkin  30011  measssd  30059  elmbfmvol2  30110  omssubadd  30143  sibfinima  30182  eulerpartlemr  30217  eulerpartlemgf  30222  fiblem  30241  domprobmeas  30253  ballotlemscr  30361  ballotlemfg  30368  ballotlemfrc  30369  ballotlemfrceq  30371  ballotlemrinv0  30375  bnj563  30521  bnj658  30529  bnj667  30530  bnj570  30683  bnj938  30715  bnj1001  30736  bnj1006  30737  bnj1049  30750  bnj1121  30761  bnj1173  30778  bnj1177  30782  bnj1245  30790  bnj1311  30800  bnj1321  30803  bnj1388  30809  bnj1398  30810  bnj1415  30814  bnj1417  30817  bnj1421  30818  bnj1442  30825  bnj1452  30828  bnj1489  30832  bnj1312  30834  pconntop  30915  sconnpconn  30917  cvmcn  30952  cvmliftlem10  30984  fundmpss  31368  sltres  31518  noseponlem  31522  funpartfun  31692  outsideofcol  31882  fnebas  31981  filnetlem3  32017  phpreu  33025  matunitlindflem1  33037  matunitlindflem2  33038  matunitlindf  33039  poimirlem26  33067  itg2addnc  33096  istotbnd3  33202  totbndmet  33203  sstotbnd2  33205  sstotbnd  33206  equivtotbnd  33209  bndmet  33212  totbndbnd  33220  prdstotbnd  33225  smgrpismgmOLD  33293  mndoissmgrpOLD  33299  crngorngo  33431  prrngorngo  33482  divrngpr  33484  ollat  33980  omlol  34007  cvlatl  34092  hlomcmcv  34123  2dim  34236  1dimN  34237  lcfl8b  36273  lclkrlem2  36301  lclkrslem1  36306  lclkrslem2  36307  lcfrlem9  36319  mapdval2N  36399  mapdordlem2  36406  mapdrvallem2  36414  nacsacs  36752  eldiophelnn0  36807  lnmlmod  37129  lnrring  37163  mncply  37188  idomrootle  37254  idomodle  37255  areaquad  37283  nznngen  37997  binomcxplemcvg  38035  2uasbanh  38259  rabidim1  38774  fompt  38853  disjinfi  38854  mbfdmssre  39524  stoweidlem14  39538  stoweidlem16  39540  stoweidlem24  39548  stoweidlem51  39575  stoweidlem54  39578  etransclem32  39790  sge0fodjrnlem  39940  preimagelt  40219  preimalegt  40220  pimrecltpos  40226  pimrecltneg  40240  smfaddlem1  40278  smflimsuplem7  40339  ndmafv  40524  evenz  40842  oddz  40843  gbeeven  40937  gboodd  40938  rnghmsubcsetclem1  41263  funcrngcsetcALT  41287  rhmsubcsetclem1  41309  rhmsubcrngclem1  41315  ssnn0ssfz  41415  elbigof  41640  digvalnn0  41685
  Copyright terms: Public domain W3C validator