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

Theorem simplbi 485
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 482 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 383
This theorem is referenced by:  an3  638  3simpaOLD  1143  xoror  1619  sbequ2  2051  rabidim1  3266  reurex  3309  eqimss  3806  pssss  3852  eldifi  3883  elinel1  3950  ssunsn2  4493  pwssun  5153  sopo  5187  wefr  5239  opelxp1  5290  relop  5411  ssrelrn  5453  ordtr  5880  funmo  6047  funrel  6048  fnfun  6128  ffn  6185  f1f  6241  f1of1  6277  f1ofo  6285  isof1o  6716  eqopi  7351  1st2nd2  7354  reldmtpos  7512  swoer  7926  erdisj  7946  ecopover  8004  sdomdom  8137  mapfien  8469  inf3lemd  8688  cardprclem  9005  infxpenlem  9036  cardinfima  9120  dfac5lem4  9149  domtriomlem  9466  smobeth  9610  fpwwe2lem6  9659  fpwwe2lem7  9660  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  axrnegex  10185  axpre-sup  10192  zre  11583  nnssz  11599  ixxss1  12398  ixxss2  12399  ixxss12  12400  lbioo  12411  ubioo  12412  iccss2  12449  rge0ssre  12487  elfzuz  12545  uzdisj  12620  nn0disj  12663  0wrd0  13527  splfv1  13715  sqrlem6  14196  rlimf  14440  lo1f  14457  lo1dm  14458  o1f  14468  o1dm  14469  mertenslem2  14824  fprodge0  14930  divalglem9  15332  bitsinv2  15373  bitsf1ocnv  15374  gcdcllem1  15429  coprmproddvdslem  15583  prmnn  15595  prmuz2  15615  phimullem  15691  hashgcdlem  15700  1arith  15838  ramtlecl  15911  0ramcl  15934  firest  16301  acsmre  16520  posprs  17157  latpos  17258  clatpos  17318  dlatl  17403  pslem  17414  tsrlemax  17428  tsrps  17429  sgrpmgm  17497  mndsgrp  17507  grpmnd  17637  nsgsubg  17834  ghmgrp1  17870  ghmgrp2  17871  gimghm  17914  gagrp  17932  gaset  17933  psgneu  18133  efgredeu  18372  ablgrp  18405  cmnmnd  18415  cyggenod2  18494  cyggrp  18498  ablfac2  18696  crngring  18766  dvdsrcl  18857  unitcl  18867  brric2  18955  drngring  18964  subrgring  18993  subrgrcl  18995  srngrhm  19061  lmimlmhm  19277  lveclmod  19319  2idlcpbl  19449  qus1  19450  qusrhm  19452  lpirring  19467  nzrring  19476  domnnzr  19510  fldidom  19520  assalmod  19534  assaring  19535  assasca  19536  cygznlem1  20130  cygznlem3  20133  lbslinds  20389  gsummatr01lem1  20680  topontop  20938  tpstop  20962  clsval2  21075  mretopd  21117  neiptoptop  21156  perftop  21181  restfpw  21204  cntop1  21265  cntop2  21266  cnptop1  21267  cnptop2  21268  cnprcl  21270  t1ficld  21352  t0top  21354  t1top  21355  haustop  21356  regtop  21358  nrmtop  21361  cnrmtop  21362  pnrmnrm  21365  cmptop  21419  discmp  21422  tgcmp  21425  uncmp  21427  conndisj  21440  conntop  21441  1stctop  21467  llytop  21496  nllytop  21497  hmeocn  21784  filfbas  21872  ufilfil  21928  flimtop  21989  flimfil  21993  alexsublem  22068  ptcmplem3  22078  tsmsfbas  22151  tsmslem1  22152  tsmsgsum  22162  tsmssubm  22166  tsmsres  22167  tsmsf1o  22168  tsmsmhm  22169  tsmsadd  22170  tsmsxplem1  22176  tsmsxplem2  22177  tsmsxp  22178  tlmtmd  22210  tlmlmod  22212  tlmtrg  22213  tvctlm  22220  ressust  22288  uspreg  22298  ucncn  22309  neipcfilu  22320  cuspusp  22324  isxmet2d  22352  metxmet  22359  xmstps  22478  msxms  22479  xmsxmet  22481  msmet  22482  stdbdxmet  22540  nrgngp  22686  nlmngp  22701  nlmlmod  22702  nlmnrg  22703  nvcnlm  22720  nmoi  22752  nghmrcl1  22756  nghmrcl2  22757  nmhmrcl1  22771  nmhmrcl2  22772  qdensere  22793  xrge0gsumle  22856  xrge0tsms  22857  metds0  22873  metdstri  22874  metdsre  22876  metdseq0  22877  metdscnlem  22878  metnrmlem1a  22881  metnrmlem1  22882  icopnfcnv  22961  cvsclm  23145  cmetmet  23303  cmsms  23364  hlbn  23378  ovolicc2lem5  23509  mblss  23519  mbff  23613  mbfres  23631  mbfadd  23648  mbfsub  23649  i1fmbf  23662  mbfmul  23713  bddmulibl  23825  limcmpt  23867  c1liplem1  23979  c1lip2  23981  fta1glem1  24145  fta1glem2  24146  fta1g  24147  fta1b  24149  ply1pid  24159  aacn  24292  ulmf2  24358  logdmnrp  24608  logdmss  24609  logcnlem2  24610  logcnlem3  24611  logcnlem4  24612  logcnlem5  24613  logcn  24614  dvloglem  24615  logf1o2  24617  efopnlem1  24623  logtayl2  24629  cxpcn  24707  cxpcn3lem  24709  cxpcn3  24710  resqrtcn  24711  atandmneg  24854  atandmcj  24857  cosatan  24869  cosatanne0  24870  birthdaylem1  24899  areacl  24910  cxp2lim  24924  jensenlem2  24935  jensen  24936  sqff1o  25129  dvdsmulf1o  25141  lgsqrlem1  25292  lgsqrlem2  25293  lgsqrlem3  25294  lgsqrlem4  25295  lgseisenlem3  25323  chebbnd1  25382  chtppilim  25385  chpchtlim  25389  chpo1ub  25390  dchrmusumlema  25403  dchrvmasumiflem1  25411  dchrisum0lema  25424  dchrisum0lem2  25428  selberg3lem2  25468  pntrsumo1  25475  selbergsb  25485  pnt2  25523  tglineeltr  25747  axcontlem2  26066  axcontlem7  26071  axcontlem8  26072  uhgr0vb  26188  lfuhgr1v0e  26369  fusgrusgr  26437  uvtxisvtx  26516  nbupgruvtxres  26537  cusgrusgr  26550  trliswlk  26829  clwlkiswlk  26905  clwwlkclwwlkn  27185  eupthistrl  27391  frgrusgr  27442  clwwnonrepclwwnon  27529  ablogrpo  27741  bnnv  28062  hlobn  28084  hcauseq  28382  hlimseqi  28386  hlimveci  28387  shss  28407  sh0  28413  chsh  28421  lnopf  29058  bdopln  29060  hmopf  29073  lnfnf  29083  unopf1o  29115  elunop2  29212  elpjhmop  29384  stcltrlem1  29475  mdslle1i  29516  mdslle2i  29517  rabexgfGS  29678  ssnnssfz  29889  tospos  29998  ogrpgrp  30043  ogrpinvOLD  30055  xrge0tsmsd  30125  ofldfld  30150  ofldlt1  30153  ofldchr  30154  isarchiofld  30157  reofld  30180  rearchi  30182  creftop  30253  lmxrge0  30338  qqhrhm  30373  esumpcvgval  30480  dynkin  30570  measssd  30618  elmbfmvol2  30669  omssubadd  30702  sibfinima  30741  eulerpartlemr  30776  eulerpartlemgf  30781  fiblem  30800  domprobmeas  30812  ballotlemscr  30920  ballotlemfg  30927  ballotlemfrc  30928  ballotlemfrceq  30930  ballotlemrinv0  30934  chtvalz  31047  bnj563  31151  bnj658  31159  bnj667  31160  bnj570  31313  bnj938  31345  bnj1001  31366  bnj1006  31367  bnj1049  31380  bnj1121  31391  bnj1173  31408  bnj1177  31412  bnj1245  31420  bnj1311  31430  bnj1321  31433  bnj1388  31439  bnj1398  31440  bnj1415  31444  bnj1417  31447  bnj1421  31448  bnj1442  31455  bnj1452  31458  bnj1489  31462  bnj1312  31464  pconntop  31545  sconnpconn  31547  cvmcn  31582  cvmliftlem10  31614  fundmpss  32002  sltres  32152  noseponlem  32154  funpartfun  32387  outsideofcol  32577  fnebas  32676  filnetlem3  32712  phpreu  33726  matunitlindflem1  33738  matunitlindflem2  33739  matunitlindf  33740  poimirlem26  33768  itg2addnc  33796  istotbnd3  33902  totbndmet  33903  sstotbnd2  33905  sstotbnd  33906  equivtotbnd  33909  bndmet  33912  totbndbnd  33920  prdstotbnd  33925  smgrpismgmOLD  33993  mndoissmgrpOLD  33999  crngorngo  34131  prrngorngo  34182  divrngpr  34184  dfxrn2  34480  symrelim  34647  ollat  35022  omlol  35049  cvlatl  35134  hlomcmcv  35165  2dim  35278  1dimN  35279  lcfl8b  37314  lclkrlem2  37342  lclkrslem1  37347  lclkrslem2  37348  lcfrlem9  37360  mapdval2N  37440  mapdordlem2  37447  mapdrvallem2  37455  nacsacs  37798  eldiophelnn0  37853  lnmlmod  38175  lnrring  38208  mncply  38233  idomrootle  38299  idomodle  38300  areaquad  38328  nznngen  39041  binomcxplemcvg  39079  2uasbanh  39302  fompt  39899  disjinfi  39900  climxrre  40500  mbfdmssre  40734  stoweidlem14  40748  stoweidlem16  40750  stoweidlem24  40758  stoweidlem51  40785  stoweidlem54  40788  etransclem32  41000  sge0fodjrnlem  41150  preimagelt  41432  preimalegt  41433  pimrecltpos  41439  pimrecltneg  41453  smfaddlem1  41491  smflimsuplem7  41552  ndmafv  41740  evenz  42071  oddz  42072  gbeeven  42170  gbowodd  42171  rnghmsubcsetclem1  42503  funcrngcsetcALT  42527  rhmsubcsetclem1  42549  rhmsubcrngclem1  42555  ssnn0ssfz  42655  elbigof  42876  digvalnn0  42921
  Copyright terms: Public domain W3C validator