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  1469  sbequ2  1880  rabidim1  3112  reurex  3155  eqimss  3649  pssss  3694  eldifi  3724  elinel1  3791  ssunsn2  4350  pwssun  5010  sopo  5042  wefr  5094  opelxp1  5140  relop  5261  ssrelrn  5304  ordtr  5725  funmo  5892  funrel  5893  fnfun  5976  ffn  6032  f1f  6088  f1of1  6123  f1ofo  6131  isof1o  6558  eqopi  7187  1st2nd2  7190  reldmtpos  7345  swoer  7757  erdisj  7779  ecopover  7836  ecopoverOLD  7837  sdomdom  7968  mapfien  8298  inf3lemd  8509  cardprclem  8790  infxpenlem  8821  cardinfima  8905  dfac5lem4  8934  domtriomlem  9249  smobeth  9393  fpwwe2lem6  9442  fpwwe2lem7  9443  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  axrnegex  9968  axpre-sup  9975  zre  11366  nnssz  11382  ixxss1  12178  ixxss2  12179  ixxss12  12180  lbioo  12191  ubioo  12192  iccss2  12229  rge0ssre  12265  elfzuz  12323  uzdisj  12397  nn0disj  12439  0wrd0  13314  splfv1  13487  sqrlem6  13969  rlimf  14213  lo1f  14230  lo1dm  14231  o1f  14241  o1dm  14242  mertenslem2  14598  fprodge0  14705  divalglem9  15105  bitsinv2  15146  bitsf1ocnv  15147  gcdcllem1  15202  coprmproddvdslem  15357  prmnn  15369  prmuz2  15389  phimullem  15465  hashgcdlem  15474  1arith  15612  ramtlecl  15685  0ramcl  15708  firest  16074  acsmre  16294  posprs  16930  latpos  17031  clatpos  17091  dlatl  17176  pslem  17187  tsrlemax  17201  tsrps  17202  sgrpmgm  17270  mndsgrp  17280  grpmnd  17410  nsgsubg  17607  ghmgrp1  17643  ghmgrp2  17644  gimghm  17687  gagrp  17706  gaset  17707  psgneu  17907  efgredeu  18146  ablgrp  18179  cmnmnd  18189  cyggenod2  18268  cyggrp  18272  ablfac2  18469  crngring  18539  dvdsrcl  18630  unitcl  18640  brric2  18726  drngring  18735  subrgring  18764  subrgrcl  18766  srngrhm  18832  lmimlmhm  19045  lveclmod  19087  2idlcpbl  19215  qus1  19216  qusrhm  19218  lpirring  19233  nzrring  19242  domnnzr  19276  fldidom  19286  assalmod  19300  assaring  19301  assasca  19302  cygznlem1  19896  cygznlem3  19899  lbslinds  20153  gsummatr01lem1  20442  topontop  20699  tpstop  20722  clsval2  20835  mretopd  20877  neiptoptop  20916  perftop  20941  restfpw  20964  cntop1  21025  cntop2  21026  cnptop1  21027  cnptop2  21028  cnprcl  21030  t1ficld  21112  t0top  21114  t1top  21115  haustop  21116  regtop  21118  nrmtop  21121  cnrmtop  21122  pnrmnrm  21125  cmptop  21179  discmp  21182  tgcmp  21185  uncmp  21187  conndisj  21200  conntop  21201  1stctop  21227  llytop  21256  nllytop  21257  hmeocn  21544  filfbas  21633  ufilfil  21689  flimtop  21750  flimfil  21754  alexsublem  21829  ptcmplem3  21839  tsmsfbas  21912  tsmslem1  21913  tsmsgsum  21923  tsmssubm  21927  tsmsres  21928  tsmsf1o  21929  tsmsmhm  21930  tsmsadd  21931  tsmsxplem1  21937  tsmsxplem2  21938  tsmsxp  21939  tlmtmd  21971  tlmlmod  21973  tlmtrg  21974  tvctlm  21981  ressust  22049  uspreg  22059  ucncn  22070  neipcfilu  22081  cuspusp  22085  isxmet2d  22113  metxmet  22120  xmstps  22239  msxms  22240  xmsxmet  22242  msmet  22243  stdbdxmet  22301  nrgngp  22447  nlmngp  22462  nlmlmod  22463  nlmnrg  22464  nvcnlm  22481  nmoi  22513  nghmrcl1  22517  nghmrcl2  22518  nmhmrcl1  22532  nmhmrcl2  22533  qdensere  22554  xrge0gsumle  22617  xrge0tsms  22618  metds0  22634  metdstri  22635  metdsre  22637  metdseq0  22638  metdscnlem  22639  metnrmlem1a  22642  metnrmlem1  22643  icopnfcnv  22722  cvsclm  22907  cmetmet  23065  cmsms  23126  hlbn  23140  ovolicc2lem5  23270  mblss  23280  mbff  23375  mbfres  23392  mbfadd  23409  mbfsub  23410  i1fmbf  23423  mbfmul  23474  bddmulibl  23586  limcmpt  23628  c1liplem1  23740  c1lip2  23742  fta1glem1  23906  fta1glem2  23907  fta1g  23908  fta1b  23910  ply1pid  23920  aacn  24053  ulmf2  24119  logdmnrp  24368  logdmss  24369  logcnlem2  24370  logcnlem3  24371  logcnlem4  24372  logcnlem5  24373  logcn  24374  dvloglem  24375  logf1o2  24377  efopnlem1  24383  logtayl2  24389  cxpcn  24467  cxpcn3lem  24469  cxpcn3  24470  resqrtcn  24471  atandmneg  24614  atandmcj  24617  cosatan  24629  cosatanne0  24630  birthdaylem1  24659  areacl  24670  cxp2lim  24684  jensenlem2  24695  jensen  24696  sqff1o  24889  dvdsmulf1o  24901  lgsqrlem1  25052  lgsqrlem2  25053  lgsqrlem3  25054  lgsqrlem4  25055  lgseisenlem3  25083  chebbnd1  25142  chtppilim  25145  chpchtlim  25149  chpo1ub  25150  dchrmusumlema  25163  dchrvmasumiflem1  25171  dchrisum0lema  25184  dchrisum0lem2  25188  selberg3lem2  25228  pntrsumo1  25235  selbergsb  25245  pnt2  25283  tglineeltr  25507  axcontlem2  25826  axcontlem7  25831  axcontlem8  25832  uhgr0vb  25948  lfuhgr1v0e  26127  fusgrusgr  26195  nbupgruvtxres  26289  cusgrusgr  26296  trliswlk  26575  clwlkiswlk  26651  eupthistrl  27051  frgrusgr  27104  ablogrpo  27371  bnnv  27692  hlobn  27714  hcauseq  28012  hlimseqi  28016  hlimveci  28017  shss  28037  sh0  28043  chsh  28051  lnopf  28688  bdopln  28690  hmopf  28703  lnfnf  28713  unopf1o  28745  elunop2  28842  elpjhmop  29014  stcltrlem1  29105  mdslle1i  29146  mdslle2i  29147  rabexgfGS  29312  ssnnssfz  29523  tospos  29632  ogrpgrp  29677  ogrpinvOLD  29689  xrge0tsmsd  29759  ofldfld  29784  ofldlt1  29787  ofldchr  29788  isarchiofld  29791  reofld  29814  rearchi  29816  creftop  29887  lmxrge0  29972  qqhrhm  30007  esumpcvgval  30114  dynkin  30204  measssd  30252  elmbfmvol2  30303  omssubadd  30336  sibfinima  30375  eulerpartlemr  30410  eulerpartlemgf  30415  fiblem  30434  domprobmeas  30446  ballotlemscr  30554  ballotlemfg  30561  ballotlemfrc  30562  ballotlemfrceq  30564  ballotlemrinv0  30568  chtvalz  30681  bnj563  30787  bnj658  30795  bnj667  30796  bnj570  30949  bnj938  30981  bnj1001  31002  bnj1006  31003  bnj1049  31016  bnj1121  31027  bnj1173  31044  bnj1177  31048  bnj1245  31056  bnj1311  31066  bnj1321  31069  bnj1388  31075  bnj1398  31076  bnj1415  31080  bnj1417  31083  bnj1421  31084  bnj1442  31091  bnj1452  31094  bnj1489  31098  bnj1312  31100  pconntop  31181  sconnpconn  31183  cvmcn  31218  cvmliftlem10  31250  fundmpss  31640  sltres  31789  noseponlem  31791  funpartfun  32025  outsideofcol  32215  fnebas  32314  filnetlem3  32350  phpreu  33364  matunitlindflem1  33376  matunitlindflem2  33377  matunitlindf  33378  poimirlem26  33406  itg2addnc  33435  istotbnd3  33541  totbndmet  33542  sstotbnd2  33544  sstotbnd  33545  equivtotbnd  33548  bndmet  33551  totbndbnd  33559  prdstotbnd  33564  smgrpismgmOLD  33632  mndoissmgrpOLD  33638  crngorngo  33770  prrngorngo  33821  divrngpr  33823  ollat  34319  omlol  34346  cvlatl  34431  hlomcmcv  34462  2dim  34575  1dimN  34576  lcfl8b  36612  lclkrlem2  36640  lclkrslem1  36645  lclkrslem2  36646  lcfrlem9  36658  mapdval2N  36738  mapdordlem2  36745  mapdrvallem2  36753  nacsacs  37091  eldiophelnn0  37146  lnmlmod  37468  lnrring  37501  mncply  37526  idomrootle  37592  idomodle  37593  areaquad  37621  nznngen  38335  binomcxplemcvg  38373  2uasbanh  38597  fompt  39195  disjinfi  39196  mbfdmssre  39980  stoweidlem14  39994  stoweidlem16  39996  stoweidlem24  40004  stoweidlem51  40031  stoweidlem54  40034  etransclem32  40246  sge0fodjrnlem  40396  preimagelt  40675  preimalegt  40676  pimrecltpos  40682  pimrecltneg  40696  smfaddlem1  40734  smflimsuplem7  40795  ndmafv  40983  evenz  41308  oddz  41309  gbeeven  41407  gbowodd  41408  rnghmsubcsetclem1  41740  funcrngcsetcALT  41764  rhmsubcsetclem1  41786  rhmsubcrngclem1  41792  ssnn0ssfz  41892  elbigof  42113  digvalnn0  42158
  Copyright terms: Public domain W3C validator