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

Theorem simplbi 487
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 207 . 2 (𝜑 → (𝜓𝜒))
32simpld 484 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  an3  641  3simpaOLD  1172  xoror  1625  sbequ2  2062  rabidim1  3306  reurex  3349  eqimss  3854  pssss  3900  eldifi  3931  elinel1  3998  ssunsn2  4548  pwssun  5215  sopo  5249  wefr  5301  opelxp1  5350  relop  5474  ssrelrn  5516  ordtr  5950  funmo  6113  funrel  6114  fnfun  6195  ffn  6252  f1f  6312  f1of1  6348  f1ofo  6356  isof1o  6793  eqopi  7430  1st2nd2  7433  reldmtpos  7591  swoer  8005  erdisj  8025  ecopover  8083  sdomdom  8216  mapfien  8548  inf3lemd  8767  cardprclem  9084  infxpenlem  9115  cardinfima  9199  dfac5lem4  9228  domtriomlem  9545  smobeth  9689  fpwwe2lem6  9738  fpwwe2lem7  9739  fpwwe2lem12  9744  fpwwe2lem13  9745  fpwwe2  9746  axrnegex  10264  axpre-sup  10271  zre  11643  nnssz  11659  ixxss1  12407  ixxss2  12408  ixxss12  12409  lbioo  12420  ubioo  12421  iccss2  12458  rge0ssre  12496  elfzuz  12557  uzdisj  12632  nn0disj  12675  0wrd0  13538  splfv1  13726  sqrlem6  14207  rlimf  14451  lo1f  14468  lo1dm  14469  o1f  14479  o1dm  14480  mertenslem2  14834  fprodge0  14940  divalglem9  15340  bitsinv2  15380  bitsf1ocnv  15381  gcdcllem1  15436  coprmproddvdslem  15590  prmnn  15602  prmuz2  15622  phimullem  15697  hashgcdlem  15706  1arith  15844  ramtlecl  15917  0ramcl  15940  firest  16294  acsmre  16513  posprs  17150  latpos  17251  clatpos  17311  dlatl  17396  pslem  17407  tsrlemax  17421  tsrps  17422  sgrpmgm  17490  mndsgrp  17500  grpmnd  17630  nsgsubg  17824  ghmgrp1  17860  ghmgrp2  17861  gimghm  17904  gagrp  17922  gaset  17923  psgneu  18123  efgredeu  18362  ablgrp  18395  cmnmnd  18405  cyggenod2  18484  cyggrp  18488  ablfac2  18686  crngring  18756  dvdsrcl  18847  unitcl  18857  brric2  18945  drngring  18954  subrgring  18983  subrgrcl  18985  srngrhm  19051  lmimlmhm  19267  lveclmod  19309  2idlcpbl  19439  qus1  19440  qusrhm  19442  lpirring  19457  nzrring  19466  domnnzr  19500  fldidom  19510  assalmod  19524  assaring  19525  assasca  19526  cygznlem1  20118  cygznlem3  20121  lbslinds  20379  gsummatr01lem1  20670  topontop  20928  tpstop  20952  clsval2  21065  mretopd  21107  neiptoptop  21146  perftop  21171  restfpw  21194  cntop1  21255  cntop2  21256  cnptop1  21257  cnptop2  21258  cnprcl  21260  t1ficld  21342  t0top  21344  t1top  21345  haustop  21346  regtop  21348  nrmtop  21351  cnrmtop  21352  pnrmnrm  21355  cmptop  21409  discmp  21412  tgcmp  21415  uncmp  21417  conndisj  21430  conntop  21431  1stctop  21457  llytop  21486  nllytop  21487  hmeocn  21774  filfbas  21862  ufilfil  21918  flimtop  21979  flimfil  21983  alexsublem  22058  ptcmplem3  22068  tsmsfbas  22141  tsmslem1  22142  tsmsgsum  22152  tsmssubm  22156  tsmsres  22157  tsmsf1o  22158  tsmsmhm  22159  tsmsadd  22160  tsmsxplem1  22166  tsmsxplem2  22167  tsmsxp  22168  tlmtmd  22200  tlmlmod  22202  tlmtrg  22203  tvctlm  22210  ressust  22278  uspreg  22288  ucncn  22299  neipcfilu  22310  cuspusp  22314  isxmet2d  22342  metxmet  22349  xmstps  22468  msxms  22469  xmsxmet  22471  msmet  22472  stdbdxmet  22530  nrgngp  22676  nlmngp  22691  nlmlmod  22692  nlmnrg  22693  nvcnlm  22710  nmoi  22742  nghmrcl1  22746  nghmrcl2  22747  nmhmrcl1  22761  nmhmrcl2  22762  qdensere  22783  xrge0gsumle  22846  xrge0tsms  22847  metds0  22863  metdstri  22864  metdsre  22866  metdseq0  22867  metdscnlem  22868  metnrmlem1a  22871  metnrmlem1  22872  icopnfcnv  22951  cvsclm  23135  cmetmet  23294  cmsms  23355  hlbn  23369  ovolicc2lem5  23501  mblss  23511  mbff  23605  mbfres  23624  mbfadd  23641  mbfsub  23642  i1fmbf  23655  mbfmul  23706  bddmulibl  23818  limcmpt  23860  c1liplem1  23972  c1lip2  23974  fta1glem1  24138  fta1glem2  24139  fta1g  24140  fta1b  24142  ply1pid  24152  aacn  24285  ulmf2  24351  logdmnrp  24600  logdmss  24601  logcnlem2  24602  logcnlem3  24603  logcnlem4  24604  logcnlem5  24605  logcn  24606  dvloglem  24607  logf1o2  24609  efopnlem1  24615  logtayl2  24621  cxpcn  24699  cxpcn3lem  24701  cxpcn3  24702  resqrtcn  24703  atandmneg  24846  atandmcj  24849  cosatan  24861  cosatanne0  24862  birthdaylem1  24891  areacl  24902  cxp2lim  24916  jensenlem2  24927  jensen  24928  sqff1o  25121  dvdsmulf1o  25133  lgsqrlem1  25284  lgsqrlem2  25285  lgsqrlem3  25286  lgsqrlem4  25287  lgseisenlem3  25315  chebbnd1  25374  chtppilim  25377  chpchtlim  25381  chpo1ub  25382  dchrmusumlema  25395  dchrvmasumiflem1  25403  dchrisum0lema  25416  dchrisum0lem2  25420  selberg3lem2  25460  pntrsumo1  25467  selbergsb  25477  pnt2  25515  tglineeltr  25739  axcontlem2  26058  axcontlem7  26063  axcontlem8  26064  uhgr0vb  26180  lfuhgr1v0e  26361  fusgrusgr  26429  uvtxisvtx  26508  nbupgruvtxres  26529  cusgrusgr  26542  trliswlk  26821  clwlkiswlk  26897  clwwlkclwwlkn  27177  eupthistrl  27383  frgrusgr  27434  clwwnonrepclwwnon  27521  ablogrpo  27729  bnnv  28049  hlobn  28071  hcauseq  28369  hlimseqi  28373  hlimveci  28374  shss  28394  sh0  28400  chsh  28408  lnopf  29045  bdopln  29047  hmopf  29060  lnfnf  29070  unopf1o  29102  elunop2  29199  elpjhmop  29371  stcltrlem1  29462  mdslle1i  29503  mdslle2i  29504  rabexgfGS  29664  ssnnssfz  29875  tospos  29982  ogrpgrp  30027  ogrpinvOLD  30039  xrge0tsmsd  30109  ofldfld  30134  ofldlt1  30137  ofldchr  30138  isarchiofld  30141  reofld  30164  rearchi  30166  creftop  30237  lmxrge0  30322  qqhrhm  30357  esumpcvgval  30464  dynkin  30554  measssd  30602  elmbfmvol2  30653  omssubadd  30686  sibfinima  30725  eulerpartlemr  30760  eulerpartlemgf  30765  fiblem  30784  domprobmeas  30796  ballotlemscr  30904  ballotlemfg  30911  ballotlemfrc  30912  ballotlemfrceq  30914  ballotlemrinv0  30918  chtvalz  31031  bnj563  31134  bnj658  31142  bnj667  31143  bnj570  31296  bnj938  31328  bnj1001  31349  bnj1006  31350  bnj1049  31363  bnj1121  31374  bnj1173  31391  bnj1177  31395  bnj1245  31403  bnj1311  31413  bnj1321  31416  bnj1388  31422  bnj1398  31423  bnj1415  31427  bnj1417  31430  bnj1421  31431  bnj1442  31438  bnj1452  31441  bnj1489  31445  bnj1312  31447  pconntop  31528  sconnpconn  31530  cvmcn  31565  cvmliftlem10  31597  fundmpss  31984  sltres  32134  noseponlem  32136  funpartfun  32369  outsideofcol  32559  fnebas  32658  filnetlem3  32694  phpreu  33704  matunitlindflem1  33716  matunitlindflem2  33717  matunitlindf  33718  poimirlem26  33746  itg2addnc  33774  istotbnd3  33879  totbndmet  33880  sstotbnd2  33882  sstotbnd  33883  equivtotbnd  33886  bndmet  33889  totbndbnd  33897  prdstotbnd  33902  smgrpismgmOLD  33970  mndoissmgrpOLD  33976  crngorngo  34108  prrngorngo  34159  divrngpr  34161  dfxrn2  34449  symrelim  34616  ollat  34991  omlol  35018  cvlatl  35103  hlomcmcv  35134  2dim  35248  1dimN  35249  lcfl8b  37282  lclkrlem2  37310  lclkrslem1  37315  lclkrslem2  37316  lcfrlem9  37328  mapdval2N  37408  mapdordlem2  37415  mapdrvallem2  37423  nacsacs  37771  eldiophelnn0  37826  lnmlmod  38147  lnrring  38180  mncply  38205  idomrootle  38271  idomodle  38272  areaquad  38299  nznngen  39012  binomcxplemcvg  39050  2uasbanh  39272  fompt  39865  disjinfi  39866  climxrre  40459  mbfdmssre  40693  stoweidlem14  40707  stoweidlem16  40709  stoweidlem24  40717  stoweidlem51  40744  stoweidlem54  40747  etransclem32  40959  sge0fodjrnlem  41109  preimagelt  41391  preimalegt  41392  pimrecltpos  41398  pimrecltneg  41412  smfaddlem1  41450  smflimsuplem7  41511  ndmafv  41726  dfafv23  41839  dfatcolem  41841  dfatco  41842  evenz  42115  oddz  42116  gbeeven  42214  gbowodd  42215  rnghmsubcsetclem1  42540  funcrngcsetcALT  42564  rhmsubcsetclem1  42586  rhmsubcrngclem1  42592  ssnn0ssfz  42692  elbigof  42913  digvalnn0  42958
  Copyright terms: Public domain W3C validator