Theorem simplbi 497

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi	⊢ (𝜑 → 𝜓)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 494	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  an3  655  xoror  1513  euex  2578  rabidim1  3310  reurex  3360  eqimss  3981  pssss  4034  eldifi  4065  elinel1  4133  ssunsn2  4765  pwssun  5484  sopo  5521  wefr  5578  opelxp1  5629  relop  5756  ssrelrn  5800  ordtr  6277  funmo  6446  funrel  6447  fnfun  6529  ffn  6596  f1f  6666  f1of1  6711  f1ofo  6719  isof1o  7187  eqopi  7853  1st2nd2  7856  reldmtpos  8034  swoer  8502  ecopover  8584  sdomdom  8739  mapfien  9128  inf3lemd  9346  cardprclem  9721  infxpenlem  9753  cardinfima  9837  dfac5lem4  9866  domtriomlem  10182  smobeth  10326  fpwwe2lem5  10375  fpwwe2lem6  10376  fpwwe2lem11  10381  fpwwe2lem12  10382  fpwwe2  10383  axrnegex  10902  axpre-sup  10909  zre  12306  ixxss1  13079  ixxss2  13080  ixxss12  13081  lbioo  13092  ubioo  13093  iccss2  13132  rge0ssre  13170  elfzuz  13234  0wrd0  14224  sqrlem6  14940  rlimf  15191  lo1f  15208  lo1dm  15209  o1f  15219  o1dm  15220  mertenslem2  15578  divalglem9  16091  bitsinv2  16131  bitsf1ocnv  16132  gcdcllem1  16187  coprmproddvdslem  16348  prmnn  16360  prmuz2  16382  phimullem  16461  hashgcdlem  16470  1arith  16609  ramtlecl  16682  0ramcl  16705  firest  17124  acsmre  17342  posprs  18015  tospos  18119  latpos  18137  clatpos  18200  dlatl  18223  pslem  18271  tsrlemax  18285  tsrps  18286  sgrpmgm  18361  mndsgrp  18372  grpmnd  18565  nsgsubg  18767  ghmgrp1  18817  ghmgrp2  18818  gimghm  18861  gagrp  18879  gaset  18880  psgneu  19095  efgredeu  19339  ablgrp  19372  cmnmnd  19383  cyggenod2  19466  cyggrp  19471  dprd2dlem1  19625  dprd2da  19626  ablfac2  19673  simpggrp  19678  crngring  19776  dvdsrcl  19872  unitcl  19882  brric2  19970  drngring  19979  subrgring  20008  subrgrcl  20010  srngrhm  20092  lmimlmhm  20307  lveclmod  20349  2idlcpbl  20486  qus1  20487  qusrhm  20489  lpirring  20504  nzrring  20513  domnnzr  20547  fldidomOLD  20558  cygznlem1  20755  cygznlem3  20758  lbslinds  21021  assalmod  21048  assaring  21049  assasca  21050  gsummatr01lem1  21785  topontop  22043  tpstop  22067  mretopd  22224  neiptoptop  22263  perftop  22288  restfpw  22311  cntop1  22372  cntop2  22373  cnptop1  22374  cnptop2  22375  cnprcl  22377  t1ficld  22459  t0top  22461  t1top  22462  haustop  22463  regtop  22465  nrmtop  22468  cnrmtop  22469  pnrmnrm  22472  cmptop  22527  tgcmp  22533  conndisj  22548  conntop  22549  1stctop  22575  llytop  22604  nllytop  22605  hmeocn  22892  filfbas  22980  ufilfil  23036  flimtop  23097  flimfil  23101  alexsublem  23176  ptcmplem3  23186  tsmsfbas  23260  tsmslem1  23261  tsmsgsum  23271  tsmssubm  23275  tsmsres  23276  tsmsf1o  23277  tsmsmhm  23278  tsmsadd  23279  tsmsxplem1  23285  tsmsxplem2  23286  tsmsxp  23287  tlmtmd  23319  tlmlmod  23321  tlmtrg  23322  tvctlm  23329  ressust  23396  uspreg  23407  ucncn  23418  neipcfilu  23429  cuspusp  23433  metxmet  23468  xmstps  23587  msxms  23588  xmsxmet  23590  msmet  23591  nrgngp  23807  nlmngp  23822  nlmlmod  23823  nlmnrg  23824  nvcnlm  23841  nmoi  23873  nghmrcl1  23877  nghmrcl2  23878  nmhmrcl1  23892  nmhmrcl2  23893  qdensere  23914  xrge0gsumle  23977  xrge0tsms  23978  icopnfcnv  24086  cvsclm  24270  cphsscph  24396  cmetmet  24431  cmsms  24493  hlbn  24508  ovolicc2lem5  24666  mblss  24676  mbff  24770  mbfres  24789  i1fmbf  24820  limcmpt  25028  c1liplem1  25141  c1lip2  25143  fta1glem1  25311  fta1glem2  25312  fta1g  25313  fta1b  25315  ply1pid  25325  aacn  25458  ulmf2  25524  logdmnrp  25777  logdmss  25778  logcnlem2  25779  logcnlem3  25780  logcnlem4  25781  logcnlem5  25782  logcn  25783  dvloglem  25784  logf1o2  25786  efopnlem1  25792  logtayl2  25798  cxpcn  25879  cxpcn3lem  25881  cxpcn3  25882  resqrtcn  25883  atandmneg  26037  atandmcj  26040  cosatan  26052  cosatanne0  26053  birthdaylem1  26082  areacl  26093  cxp2lim  26107  jensenlem2  26118  jensen  26119  sqff1o  26312  dvdsmulf1o  26324  lgsqrlem1  26475  lgsqrlem2  26476  lgsqrlem3  26477  lgsqrlem4  26478  lgseisenlem3  26506  chebbnd1  26601  chtppilim  26604  chpchtlim  26608  chpo1ub  26609  dchrmusumlema  26622  dchrvmasumiflem1  26630  dchrisum0lema  26643  dchrisum0lem2  26647  selberg3lem2  26687  pntrsumo1  26694  selbergsb  26704  pnt2  26742  tglineeltr  26973  axcontlem2  27314  axcontlem7  27319  axcontlem8  27320  uhgr0vb  27423  lfuhgr1v0e  27602  fusgrusgr  27670  uvtxisvtx  27737  nbupgruvtxres  27755  cusgrusgr  27767  trliswlk  28045  clwlkiswlk  28121  clwwlkclwwlkn  28373  eupthistrl  28554  frgrusgr  28604  frgrwopreglem5  28664  clwwnonrepclwwnon  28688  ablogrpo  28888  bnnv  29207  hlobn  29229  hcauseq  29526  hlimseqi  29530  hlimveci  29531  shss  29551  sh0  29557  chsh  29565  lnopf  30200  bdopln  30202  hmopf  30215  lnfnf  30225  unopf1o  30257  elunop2  30354  elpjhmop  30526  stcltrlem1  30617  mdslle1i  30658  mdslle2i  30659  2reu2rex1  30808  2reureurex  30809  ssnnssfz  31087  xrge0tsmsd  31296  ogrpgrp  31308  ofldfld  31488  ofldlt1  31491  ofldchr  31492  isarchiofld  31495  reofld  31523  rearchi  31525  quslsm  31572  srafldlvec  31655  rgmoddim  31672  extdggt0  31711  fldextid  31713  extdgmul  31715  extdg1id  31717  ist0cld  31762  creftop  31775  lmxrge0  31881  qqhrhm  31918  esumpcvgval  32025  dynkin  32114  measssd  32162  elmbfmvol2  32213  omssubadd  32246  sibfinima  32285  eulerpartlemr  32320  eulerpartlemgf  32325  fiblem  32344  domprobmeas  32356  ballotlemscr  32464  ballotlemfg  32471  ballotlemfrc  32472  ballotlemfrceq  32474  ballotlemrinv0  32478  chtvalz  32588  bnj563  32702  bnj658  32710  bnj667  32711  bnj570  32864  bnj938  32896  bnj1001  32918  bnj1006  32919  bnj1049  32933  bnj1121  32944  bnj1173  32961  bnj1177  32965  bnj1245  32973  bnj1311  32983  bnj1321  32986  bnj1388  32992  bnj1398  32993  bnj1415  32997  bnj1417  33000  bnj1421  33001  bnj1442  33008  bnj1452  33011  bnj1489  33015  bnj1312  33017  pthacycspth  33098  pconntop  33166  sconnpconn  33168  cvmcn  33203  cvmliftlem10  33235  sate0fv0  33358  fundmpss  33719  sltres  33844  noseponlem  33846  txpss3v  34159  pprodss4v  34165  outsideofcol  34414  fnebas  34512  filnetlem3  34548  bj-nnfe  34892  bj-xpcossxp  35339  bj-rvecmod  35445  pibt2  35567  phpreu  35740  matunitlindflem1  35752  matunitlindflem2  35753  matunitlindf  35754  poimirlem26  35782  itg2addnc  35810  istotbnd3  35908  totbndmet  35909  sstotbnd2  35911  sstotbnd  35912  equivtotbnd  35915  bndmet  35918  totbndbnd  35926  prdstotbnd  35931  smgrpismgmOLD  35999  mndoissmgrpOLD  36005  crngorngo  36137  prrngorngo  36188  divrngpr  36190  xrnss3v  36481  dfxrn2  36485  symrelim  36652  eqvrelsym  36697  eqvreltr  36699  disjorimxrn  36835  ollat  37206  omlol  37233  cvlatl  37318  hlomcmcv  37349  2dim  37463  1dimN  37464  lcfl8b  39497  lclkrlem2  39525  lclkrslem1  39530  lclkrslem2  39531  lcfrlem9  39543  mapdval2N  39623  mapdordlem2  39630  mapdrvallem2  39638  prjcrv0  40450  nacsacs  40511  eldiophelnn0  40566  lnmlmod  40884  lnrring  40917  mncply  40942  idomrootle  41000  idomodle  41001  areaquad  41027  harval3  41105  alephiso3  41119  mnurndlem1  41852  nznngen  41887  binomcxplemcvg  41925  2uasbanh  42134  fompt  42683  disjinfi  42684  climxrre  43245  mbfdmssre  43495  stoweidlem14  43509  stoweidlem16  43511  stoweidlem24  43519  stoweidlem51  43546  stoweidlem54  43549  etransclem32  43761  sge0fodjrnlem  43908  pimrecltpos  44197  pimrecltneg  44211  smfaddlem1  44249  smflimsuplem7  44310  ndmafv  44583  dfafv23  44696  dfatcolem  44698  dfatco  44699  evenz  45034  oddz  45035  gbeeven  45158  gbowodd  45159  rnghmsubcsetclem1  45485  funcrngcsetcALT  45509  rhmsubcsetclem1  45531  rhmsubcrngclem1  45537  ssnn0ssfz  45637  elbigof  45852  digvalnn0  45897  2sphere  46047  mof0  46117  mof0ALT  46119  thincc  46257  upwordisword  46465