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

Theorem simplbi 478
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 477 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  an3  903  3simpaOLD  1144  xoror  1620  sbequ2  2048  rabidim1  3256  reurex  3299  eqimss  3798  pssss  3844  eldifi  3875  elinel1  3942  ssunsn2  4504  pwssun  5170  sopo  5204  wefr  5256  opelxp1  5307  relop  5428  ssrelrn  5470  ordtr  5898  funmo  6065  funrel  6066  fnfun  6149  ffn  6206  f1f  6262  f1of1  6297  f1ofo  6305  isof1o  6736  eqopi  7369  1st2nd2  7372  reldmtpos  7529  swoer  7941  erdisj  7961  ecopover  8018  sdomdom  8149  mapfien  8478  inf3lemd  8697  cardprclem  8995  infxpenlem  9026  cardinfima  9110  dfac5lem4  9139  domtriomlem  9456  smobeth  9600  fpwwe2lem6  9649  fpwwe2lem7  9650  fpwwe2lem12  9655  fpwwe2lem13  9656  fpwwe2  9657  axrnegex  10175  axpre-sup  10182  zre  11573  nnssz  11589  ixxss1  12386  ixxss2  12387  ixxss12  12388  lbioo  12399  ubioo  12400  iccss2  12437  rge0ssre  12473  elfzuz  12531  uzdisj  12606  nn0disj  12649  0wrd0  13517  splfv1  13706  sqrlem6  14187  rlimf  14431  lo1f  14448  lo1dm  14449  o1f  14459  o1dm  14460  mertenslem2  14816  fprodge0  14923  divalglem9  15326  bitsinv2  15367  bitsf1ocnv  15368  gcdcllem1  15423  coprmproddvdslem  15578  prmnn  15590  prmuz2  15610  phimullem  15686  hashgcdlem  15695  1arith  15833  ramtlecl  15906  0ramcl  15929  firest  16295  acsmre  16514  posprs  17150  latpos  17251  clatpos  17311  dlatl  17396  pslem  17407  tsrlemax  17421  tsrps  17422  sgrpmgm  17490  mndsgrp  17500  grpmnd  17630  nsgsubg  17827  ghmgrp1  17863  ghmgrp2  17864  gimghm  17907  gagrp  17925  gaset  17926  psgneu  18126  efgredeu  18365  ablgrp  18398  cmnmnd  18408  cyggenod2  18487  cyggrp  18491  ablfac2  18688  crngring  18758  dvdsrcl  18849  unitcl  18859  brric2  18947  drngring  18956  subrgring  18985  subrgrcl  18987  srngrhm  19053  lmimlmhm  19266  lveclmod  19308  2idlcpbl  19436  qus1  19437  qusrhm  19439  lpirring  19454  nzrring  19463  domnnzr  19497  fldidom  19507  assalmod  19521  assaring  19522  assasca  19523  cygznlem1  20117  cygznlem3  20120  lbslinds  20374  gsummatr01lem1  20663  topontop  20920  tpstop  20943  clsval2  21056  mretopd  21098  neiptoptop  21137  perftop  21162  restfpw  21185  cntop1  21246  cntop2  21247  cnptop1  21248  cnptop2  21249  cnprcl  21251  t1ficld  21333  t0top  21335  t1top  21336  haustop  21337  regtop  21339  nrmtop  21342  cnrmtop  21343  pnrmnrm  21346  cmptop  21400  discmp  21403  tgcmp  21406  uncmp  21408  conndisj  21421  conntop  21422  1stctop  21448  llytop  21477  nllytop  21478  hmeocn  21765  filfbas  21853  ufilfil  21909  flimtop  21970  flimfil  21974  alexsublem  22049  ptcmplem3  22059  tsmsfbas  22132  tsmslem1  22133  tsmsgsum  22143  tsmssubm  22147  tsmsres  22148  tsmsf1o  22149  tsmsmhm  22150  tsmsadd  22151  tsmsxplem1  22157  tsmsxplem2  22158  tsmsxp  22159  tlmtmd  22191  tlmlmod  22193  tlmtrg  22194  tvctlm  22201  ressust  22269  uspreg  22279  ucncn  22290  neipcfilu  22301  cuspusp  22305  isxmet2d  22333  metxmet  22340  xmstps  22459  msxms  22460  xmsxmet  22462  msmet  22463  stdbdxmet  22521  nrgngp  22667  nlmngp  22682  nlmlmod  22683  nlmnrg  22684  nvcnlm  22701  nmoi  22733  nghmrcl1  22737  nghmrcl2  22738  nmhmrcl1  22752  nmhmrcl2  22753  qdensere  22774  xrge0gsumle  22837  xrge0tsms  22838  metds0  22854  metdstri  22855  metdsre  22857  metdseq0  22858  metdscnlem  22859  metnrmlem1a  22862  metnrmlem1  22863  icopnfcnv  22942  cvsclm  23126  cmetmet  23284  cmsms  23345  hlbn  23359  ovolicc2lem5  23489  mblss  23499  mbff  23593  mbfres  23610  mbfadd  23627  mbfsub  23628  i1fmbf  23641  mbfmul  23692  bddmulibl  23804  limcmpt  23846  c1liplem1  23958  c1lip2  23960  fta1glem1  24124  fta1glem2  24125  fta1g  24126  fta1b  24128  ply1pid  24138  aacn  24271  ulmf2  24337  logdmnrp  24586  logdmss  24587  logcnlem2  24588  logcnlem3  24589  logcnlem4  24590  logcnlem5  24591  logcn  24592  dvloglem  24593  logf1o2  24595  efopnlem1  24601  logtayl2  24607  cxpcn  24685  cxpcn3lem  24687  cxpcn3  24688  resqrtcn  24689  atandmneg  24832  atandmcj  24835  cosatan  24847  cosatanne0  24848  birthdaylem1  24877  areacl  24888  cxp2lim  24902  jensenlem2  24913  jensen  24914  sqff1o  25107  dvdsmulf1o  25119  lgsqrlem1  25270  lgsqrlem2  25271  lgsqrlem3  25272  lgsqrlem4  25273  lgseisenlem3  25301  chebbnd1  25360  chtppilim  25363  chpchtlim  25367  chpo1ub  25368  dchrmusumlema  25381  dchrvmasumiflem1  25389  dchrisum0lema  25402  dchrisum0lem2  25406  selberg3lem2  25446  pntrsumo1  25453  selbergsb  25463  pnt2  25501  tglineeltr  25725  axcontlem2  26044  axcontlem7  26049  axcontlem8  26050  uhgr0vb  26166  lfuhgr1v0e  26345  fusgrusgr  26413  uvtxisvtx  26491  nbupgruvtxres  26512  cusgrusgr  26525  trliswlk  26804  clwlkiswlk  26880  clwwlkclwwlkn  27158  eupthistrl  27363  frgrusgr  27414  clwwnonrepclwwnon  27502  ablogrpo  27710  bnnv  28031  hlobn  28053  hcauseq  28351  hlimseqi  28355  hlimveci  28356  shss  28376  sh0  28382  chsh  28390  lnopf  29027  bdopln  29029  hmopf  29042  lnfnf  29052  unopf1o  29084  elunop2  29181  elpjhmop  29353  stcltrlem1  29444  mdslle1i  29485  mdslle2i  29486  rabexgfGS  29647  ssnnssfz  29858  tospos  29967  ogrpgrp  30012  ogrpinvOLD  30024  xrge0tsmsd  30094  ofldfld  30119  ofldlt1  30122  ofldchr  30123  isarchiofld  30126  reofld  30149  rearchi  30151  creftop  30222  lmxrge0  30307  qqhrhm  30342  esumpcvgval  30449  dynkin  30539  measssd  30587  elmbfmvol2  30638  omssubadd  30671  sibfinima  30710  eulerpartlemr  30745  eulerpartlemgf  30750  fiblem  30769  domprobmeas  30781  ballotlemscr  30889  ballotlemfg  30896  ballotlemfrc  30897  ballotlemfrceq  30899  ballotlemrinv0  30903  chtvalz  31016  bnj563  31120  bnj658  31128  bnj667  31129  bnj570  31282  bnj938  31314  bnj1001  31335  bnj1006  31336  bnj1049  31349  bnj1121  31360  bnj1173  31377  bnj1177  31381  bnj1245  31389  bnj1311  31399  bnj1321  31402  bnj1388  31408  bnj1398  31409  bnj1415  31413  bnj1417  31416  bnj1421  31417  bnj1442  31424  bnj1452  31427  bnj1489  31431  bnj1312  31433  pconntop  31514  sconnpconn  31516  cvmcn  31551  cvmliftlem10  31583  fundmpss  31971  sltres  32121  noseponlem  32123  funpartfun  32356  outsideofcol  32546  fnebas  32645  filnetlem3  32681  phpreu  33706  matunitlindflem1  33718  matunitlindflem2  33719  matunitlindf  33720  poimirlem26  33748  itg2addnc  33777  istotbnd3  33883  totbndmet  33884  sstotbnd2  33886  sstotbnd  33887  equivtotbnd  33890  bndmet  33893  totbndbnd  33901  prdstotbnd  33906  smgrpismgmOLD  33974  mndoissmgrpOLD  33980  crngorngo  34112  prrngorngo  34163  divrngpr  34165  dfxrn2  34461  symrelim  34628  ollat  35003  omlol  35030  cvlatl  35115  hlomcmcv  35146  2dim  35259  1dimN  35260  lcfl8b  37295  lclkrlem2  37323  lclkrslem1  37328  lclkrslem2  37329  lcfrlem9  37341  mapdval2N  37421  mapdordlem2  37428  mapdrvallem2  37436  nacsacs  37774  eldiophelnn0  37829  lnmlmod  38151  lnrring  38184  mncply  38209  idomrootle  38275  idomodle  38276  areaquad  38304  nznngen  39017  binomcxplemcvg  39055  2uasbanh  39279  fompt  39878  disjinfi  39879  climxrre  40485  mbfdmssre  40720  stoweidlem14  40734  stoweidlem16  40736  stoweidlem24  40744  stoweidlem51  40771  stoweidlem54  40774  etransclem32  40986  sge0fodjrnlem  41136  preimagelt  41418  preimalegt  41419  pimrecltpos  41425  pimrecltneg  41439  smfaddlem1  41477  smflimsuplem7  41538  ndmafv  41726  evenz  42053  oddz  42054  gbeeven  42152  gbowodd  42153  rnghmsubcsetclem1  42485  funcrngcsetcALT  42509  rhmsubcsetclem1  42531  rhmsubcrngclem1  42537  ssnn0ssfz  42637  elbigof  42858  digvalnn0  42903
  Copyright terms: Public domain W3C validator