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 217	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 495	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  an3  665  xoror  1525  euex  2581  reurex  3349  rabidim1  3414  pssss  4036  eldifi  4068  elinel1  4137  ssunsn2  4765  pwssun  5517  sopo  5552  wefr  5615  opelxp1  5667  relop  5799  ssrelrn  5843  ordtr  6331  funmo  6508  funrel  6509  fnfun  6592  ffn  6662  f1f  6730  f1of1  6773  f1ofo  6781  isof1o  7274  eqopi  7974  1st2nd2  7977  reldmtpos  8181  brinxper  8670  swoer  8672  ecopover  8765  sdomdom  8924  mapfien  9318  inf3lemd  9546  cardprclem  9901  infxpenlem  9933  cardinfima  10017  dfac5lem4  10046  dfac5lem4OLD  10048  domtriomlem  10362  smobeth  10507  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  axrnegex  11083  axpre-sup  11090  zre  12526  ixxss1  13314  ixxss2  13315  ixxss12  13316  lbioo  13327  ubioo  13328  iccss2  13368  rge0ssre  13407  elfzuz  13472  0wrd0  14500  01sqrexlem6  15207  rlimf  15461  lo1f  15478  lo1dm  15479  o1f  15489  o1dm  15490  mertenslem2  15848  divalglem9  16368  bitsinv2  16410  bitsf1ocnv  16411  gcdcllem1  16466  coprmproddvdslem  16629  prmnn  16641  prmuz2  16663  phimullem  16747  hashgcdlem  16756  1arith  16896  ramtlecl  16969  0ramcl  16992  firest  17393  acsmre  17616  posprs  18280  tospos  18382  latpos  18402  clatpos  18465  dlatl  18488  pslem  18536  tsrlemax  18550  tsrps  18551  chnwrd  18572  sgrpmgm  18690  mndsgrp  18706  grpmnd  18914  nsgsubg  19131  ghmgrp1  19191  ghmgrp2  19192  gimghm  19237  gagrp  19265  gaset  19266  psgneu  19479  efgredeu  19725  ablgrp  19758  cmnmnd  19770  cyggenod2  19858  cyggrp  19863  dprd2dlem1  20016  dprd2da  20017  ablfac2  20064  simpggrp  20069  ogrpgrp  20098  crngring  20224  dvdsrcl  20343  unitcl  20353  rimrhm  20472  brric2  20485  nzrringOLD  20496  subrgring  20553  subrgrcl  20555  rnghmsubcsetclem1  20610  funcrngcsetcALT  20620  rhmsubcsetclem1  20639  rhmsubcrngclem1  20645  domnnzr  20685  drngring  20715  flddrngd  20720  rng1nfld  20758  srngrhm  20824  ofldfld  20851  ofldlt1  20854  lmimlmhm  21061  lveclmod  21103  2idlelbas  21264  rng2idlsubgsubrng  21268  2idlcpblrng  21271  2idlcpbl  21272  qus1  21274  qusrhm  21276  lpirring  21331  cygznlem1  21548  cygznlem3  21551  ofldchr  21558  lbslinds  21815  assalmod  21842  assaring  21843  gsummatr01lem1  22645  topontop  22903  tpstop  22927  mretopd  23082  neiptoptop  23121  perftop  23146  restfpw  23169  cntop1  23230  cntop2  23231  cnptop1  23232  cnptop2  23233  cnprcl  23235  t1ficld  23317  t0top  23319  t1top  23320  haustop  23321  regtop  23323  nrmtop  23326  cnrmtop  23327  pnrmnrm  23330  cmptop  23385  tgcmp  23391  conndisj  23406  conntop  23407  1stctop  23433  llytop  23462  nllytop  23463  hmeocn  23750  filfbas  23838  ufilfil  23894  flimtop  23955  flimfil  23959  alexsublem  24034  ptcmplem3  24044  tsmsfbas  24118  tsmslem1  24119  tsmsgsum  24129  tsmssubm  24133  tsmsres  24134  tsmsf1o  24135  tsmsmhm  24136  tsmsadd  24137  tsmsxplem1  24143  tsmsxplem2  24144  tsmsxp  24145  tlmtmd  24177  tlmlmod  24179  tlmtrg  24180  tvctlm  24187  ressust  24253  uspreg  24263  ucncn  24274  neipcfilu  24285  cuspusp  24289  metxmet  24324  xmstps  24443  msxms  24444  xmsxmet  24446  msmet  24447  nrgngp  24652  nlmngp  24667  nlmlmod  24668  nlmnrg  24669  nvcnlm  24686  nmoi  24718  nghmrcl1  24722  nghmrcl2  24723  nmhmrcl1  24737  nmhmrcl2  24738  qdensere  24759  xrge0gsumle  24824  xrge0tsms  24825  icopnfcnv  24934  cvsclm  25118  cphsscph  25243  cmetmet  25278  cmsms  25340  hlbn  25355  ovolicc2lem5  25513  mblss  25523  mbff  25617  mbfres  25636  i1fmbf  25667  limcmpt  25875  c1liplem1  25988  c1lip2  25990  fta1glem1  26158  fta1glem2  26159  fta1g  26160  fta1b  26162  idomrootle  26163  ply1pid  26173  aacn  26308  ulmf2  26374  logdmnrp  26630  logdmss  26631  logcnlem2  26632  logcnlem3  26633  logcnlem4  26634  logcnlem5  26635  logcn  26636  dvloglem  26637  logf1o2  26639  efopnlem1  26645  logtayl2  26651  cxpcn  26734  cxpcn3lem  26736  cxpcn3  26737  resqrtcn  26738  atandmneg  26895  atandmcj  26898  cosatan  26910  cosatanne0  26911  birthdaylem1  26940  areacl  26951  cxp2lim  26965  jensenlem2  26976  jensen  26977  sqff1o  27170  mpodvdsmulf1o  27182  dvdsmulf1o  27184  lgsqrlem1  27334  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  lgseisenlem3  27365  chebbnd1  27460  chtppilim  27463  chpchtlim  27467  chpo1ub  27468  dchrmusumlema  27481  dchrvmasumiflem1  27489  dchrisum0lema  27502  dchrisum0lem2  27506  selberg3lem2  27546  pntrsumo1  27553  selbergsb  27563  pnt2  27601  ltsres  27651  noseponlem  27653  reno  28509  tglineeltr  28724  axcontlem2  29059  axcontlem7  29064  axcontlem8  29065  uhgr0vb  29166  lfuhgr1v0e  29348  fusgrusgr  29416  uvtxisvtx  29483  nbupgruvtxres  29501  cusgrusgr  29513  trliswlk  29789  clwlkiswlk  29867  clwwlkclwwlkn  30125  eupthistrl  30306  frgrusgr  30356  frgrwopreglem5  30416  clwwnonrepclwwnon  30440  ablogrpo  30643  bnnv  30962  hlobn  30984  hcauseq  31281  hlimseqi  31285  hlimveci  31286  shss  31306  sh0  31312  chsh  31320  lnopf  31955  bdopln  31957  hmopf  31970  lnfnf  31980  unopf1o  32012  elunop2  32109  elpjhmop  32281  stcltrlem1  32372  mdslle1i  32413  mdslle2i  32414  2reu2rex1  32575  2reureurex  32576  ssnnssfz  32886  xrge0tsmsd  33161  isarchiofld  33287  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  isdrng4  33386  reofld  33433  rearchi  33436  quslsm  33495  ufdidom  33632  mplvrpmga  33736  srafldlvec  33777  extdggt0  33848  fldextid  33850  extdgid  33851  extdgmul  33854  extdg1id  33857  ist0cld  34024  creftop  34037  lmxrge0  34143  qqhrhm  34180  esumpcvgval  34269  dynkin  34358  measssd  34406  elmbfmvol2  34458  omssubadd  34491  sibfinima  34530  eulerpartlemr  34565  eulerpartlemgf  34570  fiblem  34589  domprobmeas  34601  ballotlemscr  34710  ballotlemfg  34717  ballotlemfrc  34718  ballotlemfrceq  34720  ballotlemrinv0  34724  chtvalz  34820  bnj563  34933  bnj658  34941  bnj667  34942  bnj570  35094  bnj938  35126  bnj1001  35148  bnj1006  35149  bnj1049  35163  bnj1121  35174  bnj1173  35191  bnj1177  35195  bnj1245  35203  bnj1311  35213  bnj1321  35216  bnj1388  35222  bnj1398  35223  bnj1415  35227  bnj1417  35230  bnj1421  35231  bnj1442  35238  bnj1452  35241  bnj1489  35245  bnj1312  35247  pthacycspth  35392  pconntop  35460  sconnpconn  35462  cvmcn  35497  cvmliftlem10  35529  sate0fv0  35652  fundmpss  36002  txpss3v  36111  pprodss4v  36117  outsideofcol  36368  fnebas  36579  filnetlem3  36615  bj-nnfe  37081  bj-xpcossxp  37556  bj-rvecmod  37662  pibt2  37786  phpreu  37978  matunitlindflem1  37990  matunitlindflem2  37991  matunitlindf  37992  poimirlem26  38020  itg2addnc  38048  istotbnd3  38145  totbndmet  38146  sstotbnd2  38148  sstotbnd  38149  equivtotbnd  38152  bndmet  38155  totbndbnd  38163  prdstotbnd  38168  smgrpismgmOLD  38236  mndoissmgrpOLD  38242  crngorngo  38374  prrngorngo  38425  divrngpr  38427  xrnss3v  38755  dfxrn2  38759  refressn  38907  antisymressn  38908  symrelim  39017  eqvrelsym  39063  eqvreltr  39065  disjimeceqim  39178  disjorimxrn  39222  disjim  39258  disjlem14  39275  ollat  39712  omlol  39739  cvlatl  39824  hlomcmcv  39855  2dim  39969  1dimN  39970  lcfl8b  42003  lclkrlem2  42031  lclkrslem1  42036  lclkrslem2  42037  lcfrlem9  42049  mapdval2N  42129  mapdordlem2  42136  mapdrvallem2  42144  idomnnzgmulnz  42625  aks6d1c6lem3  42664  readvrec2  42845  readvrec  42846  readvcot  42848  nacsacs  43165  eldiophelnn0  43220  lnmlmod  43531  lnrring  43564  mncply  43589  idomodle  43643  areaquad  43668  dfno2  43879  harval3  43989  alephiso3  44010  mnurndlem1  44732  nznngen  44767  binomcxplemcvg  44805  2uasbanh  45012  relpf  45401  disjinfi  45646  climxrre  46200  mbfdmssre  46450  stoweidlem14  46464  stoweidlem16  46466  stoweidlem24  46474  stoweidlem51  46501  stoweidlem54  46504  etransclem32  46716  sge0fodjrnlem  46866  pimrecltpos  47158  pimrecltneg  47174  smfaddlem1  47213  smflimsuplem7  47276  ndmafv  47610  dfafv23  47723  dfatcolem  47725  dfatco  47726  evenz  48128  oddz  48129  gbeeven  48252  gbowodd  48253  sclnbgrisvtx  48347  grlimgredgex  48498  ssnn0ssfz  48847  elbigof  49052  digvalnn0  49097  2sphere  49247  mof0  49335  mof0ALT  49337  uobeq2  49898  thincc  49919  termcthin  49974