Theorem simplbi 502

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an3  672  xoror  1548  euex  2605  reurex  3373  rabidim1  3437  pssss  4028  eldifi  4070  elinel1  4101  ssunsn2  4786  pwssun  5548  sopo  5583  wefr  5646  opelxp1  5698  relop  5835  ssrelrn  5884  ordtr  6397  funmo  6577  funrel  6579  fnfun  6664  ffn  6734  f1f  6803  f1of1  6848  f1ofo  6857  isof1o  7357  eqopi  8064  1st2nd2  8067  reldmtpos  8282  brinxper  8778  swoer  8780  ecopover  8873  sdomdom  9038  mapfien  9430  inf3lemd  9658  cardprclem  10090  infxpenlem  10122  cardinfima  10206  dfac5lem4  10235  domtriomlem  10550  smobeth  10701  fpwwe2lem5  10750  fpwwe2lem6  10751  fpwwe2lem11  10756  fpwwe2lem12  10757  fpwwe2  10758  axrnegex  11277  axpre-sup  11284  zre  12727  ixxss1  13524  ixxss2  13525  ixxss12  13526  lbioo  13537  ubioo  13538  iccss2  13578  rge0ssre  13617  elfzuz  13682  0wrd0  14715  01sqrexlem6  15446  rlimf  15700  lo1f  15717  lo1dm  15718  o1f  15728  o1dm  15729  mertenslem2  16086  divalglem9  16603  bitsinv2  16645  bitsf1ocnv  16646  gcdcllem1  16701  coprmproddvdslem  16869  prmnn  16881  prmuz2  16903  phimullem  16988  hashgcdlem  16997  1arith  17137  ramtlecl  17210  0ramcl  17233  firest  17635  acsmre  17858  posprs  18522  tospos  18624  latpos  18644  clatpos  18707  dlatl  18730  pslem  18778  tsrlemax  18792  tsrps  18793  chnwrd  18814  sgrpmgm  18945  mndsgrp  18961  grpmnd  19183  nsgsubg  19400  ghmgrp1  19464  ghmgrp2  19465  gimghm  19510  gagrp  19539  gaset  19540  psgneu  19753  efgredeu  19999  ablgrp  20032  cmnmnd  20044  cyggenod2  20132  cyggrp  20137  dprd2dlem1  20290  dprd2da  20291  ablfac2  20338  simpggrp  20343  ogrpgrp  20372  crngring  20505  dvdsrcl  20628  unitcl  20638  rimrhm  20764  isbrric2  20786  nzrringOLD  20800  subrgring  20859  subrgrcl  20861  rnghmsubcsetclem1  20916  funcrngcsetcALT  20926  rhmsubcsetclem1  20945  rhmsubcrngclem1  20951  domnnzr  20991  drngring  21020  isdrng4  21025  flddrngd  21027  rng1nfld  21069  srngrhm  21135  ofldfld  21162  ofldlt1  21165  lmimlmhm  21372  lveclmod  21414  2idlelbas  21591  rng2idlsubgsubrng  21595  2idlcpblrng  21598  2idlcpbl  21599  qus1  21601  qusrhm  21603  lpirring  21688  cygznlem1  21905  cygznlem3  21908  ofldchr  21915  lbslinds  22172  assalmod  22201  assaring  22202  gsummatr01lem1  23003  matunitlindflem1  23027  matunitlindflem2  23028  matunitlindf  23029  topontop  23264  tpstop  23288  mretopd  23443  neiptoptop  23482  perftop  23507  restfpw  23530  cntop1  23591  cntop2  23592  cnptop1  23593  cnptop2  23594  cnprcl  23596  t1ficld  23678  t0top  23680  t1top  23681  haustop  23682  regtop  23684  nrmtop  23687  cnrmtop  23688  pnrmnrm  23691  cmptop  23746  tgcmp  23752  conndisj  23767  conntop  23768  1stctop  23794  llytop  23824  nllytop  23825  hmeocn  24112  filfbas  24200  ufilfil  24256  flimtop  24317  flimfil  24321  alexsublem  24396  ptcmplem3  24406  tsmsfbas  24480  tsmslem1  24481  tsmsgsum  24491  tsmssubm  24495  tsmsres  24496  tsmsf1o  24497  tsmsmhm  24498  tsmsadd  24499  tsmsxplem1  24505  tsmsxplem2  24506  tsmsxp  24507  tlmtmd  24539  tlmlmod  24541  tlmtrg  24542  tvctlm  24549  ressust  24615  uspreg  24625  ucncn  24636  neipcfilu  24647  cuspusp  24651  metxmet  24686  xmstps  24805  msxms  24806  xmsxmet  24808  msmet  24809  nrgngp  25014  nlmngp  25029  nlmlmod  25030  nlmnrg  25031  nvcnlm  25048  nmoi  25080  nghmrcl1  25084  nghmrcl2  25085  nmhmrcl1  25099  nmhmrcl2  25100  qdensere  25121  xrge0gsumle  25186  xrge0tsms  25187  icopnfcnv  25296  cvsclm  25480  cphsscph  25605  cmetmet  25640  cmsms  25702  hlbn  25717  ovolicc2lem5  25875  mblss  25885  mbff  25979  mbfres  25998  i1fmbf  26029  limcmpt  26236  c1liplem1  26349  c1lip2  26351  fta1glem1  26519  fta1glem2  26520  fta1g  26521  fta1b  26523  idomrootle  26524  ply1pid  26534  aacn  26673  ulmf2  26744  logdmnrp  27002  logdmss  27003  logcnlem2  27004  logcnlem3  27005  logcnlem4  27006  logcnlem5  27007  logcn  27008  dvloglem  27009  logf1o2  27011  efopnlem1  27017  logtayl2  27023  cxpcn  27106  cxpcn3lem  27108  cxpcn3  27109  resqrtcn  27110  atandmneg  27267  atandmcj  27270  cosatan  27282  cosatanne0  27283  birthdaylem1  27312  areacl  27323  cxp2lim  27337  jensenlem2  27348  jensen  27349  sqff1o  27542  mpodvdsmulf1o  27554  dvdsmulf1o  27556  lgsqrlem1  27706  lgsqrlem2  27707  lgsqrlem3  27708  lgsqrlem4  27709  lgseisenlem3  27737  chebbnd1  27832  chtppilim  27835  chpchtlim  27839  chpo1ub  27840  dchrmusumlema  27853  dchrvmasumiflem1  27861  dchrisum0lema  27874  dchrisum0lem2  27878  selberg3lem2  27918  pntrsumo1  27925  selbergsb  27935  pnt2  27973  ltsres  28052  noseponlem  28054  reno  28911  tglineeltr  29132  axcontlem2  29576  axcontlem7  29581  axcontlem8  29582  uhgr0vb  29683  lfuhgr1v0e  29868  fusgrusgr  29936  uvtxisvtx  30003  nbupgruvtxres  30021  cusgrusgr  30033  trliswlk  30313  clwlkiswlk  30394  clwwlkclwwlkn  30654  eupthistrl  30845  frgrusgr  30895  frgrwopreglem5  30955  clwwnonrepclwwnon  30979  ablogrpo  31182  bnnv  31501  hlobn  31523  hcauseq  31820  hlimseqi  31824  hlimveci  31825  shss  31845  sh0  31851  chsh  31859  lnopf  32494  bdopln  32496  hmopf  32509  lnfnf  32519  unopf1o  32551  elunop2  32648  elpjhmop  32820  stcltrlem1  32911  mdslle1i  32952  mdslle2i  32953  2reu2rex1  33152  2reureurex  33153  ssnnssfz  33452  xrge0tsmsd  33710  isarchiofld  33836  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnlem4  33882  edomidom  33935  reofld  33988  rearchi  33991  quslsm  34040  ufdidom  34158  mplvrpmga  34260  srafldlvec  34301  extdggt0  34372  fldextid  34374  extdgid  34375  extdgmul  34378  extdg1id  34381  ist0cld  34548  creftop  34561  lmxrge0  34667  qqhrhm  34704  esumpcvgval  34793  dynkin  34883  measssd  34931  elmbfmvol2  34982  sibfinima  35054  eulerpartlemr  35089  eulerpartlemgf  35094  fiblem  35113  domprobmeas  35125  ballotlemscr  35234  ballotlemfg  35241  ballotlemfrc  35242  ballotlemfrceq  35244  ballotlemrinv0  35248  chtvalz  35341  bnj563  35457  bnj658  35465  bnj667  35466  bnj570  35618  bnj938  35650  bnj1001  35672  bnj1006  35673  bnj1049  35687  bnj1121  35698  bnj1173  35715  bnj1177  35719  bnj1245  35727  bnj1311  35737  bnj1321  35740  bnj1388  35746  bnj1398  35747  bnj1415  35751  bnj1417  35754  bnj1421  35755  bnj1442  35762  bnj1452  35765  bnj1489  35769  bnj1312  35771  fwfffunres  35801  pthacycspth  36092  pconntop  36170  sconnpconn  36172  cvmcn  36207  cvmliftlem10  36239  sate0fv0  36362  fundmpss  36723  txpss3v  36831  pprodss4v  36837  outsideofcol  37089  fnebas  37323  filnetlem3  37359  bj-nnfe  37824  bj-xpcossxp  38315  bj-rvecmod  38421  pibt2  38545  phpreu  38732  poimirlem26  38769  itg2addnc  38797  istotbnd3  38908  totbndmet  38909  sstotbnd2  38911  sstotbnd  38912  equivtotbnd  38915  bndmet  38918  totbndbnd  38926  prdstotbnd  38931  smgrpismgmOLD  38999  mndoissmgrpOLD  39005  crngorngo  39137  prrngorngo  39188  divrngpr  39190  xrnss3v  39516  dfxrn2  39520  refressn  39668  antisymressn  39669  symrelim  39778  eqvrelsym  39824  eqvreltr  39826  disjimeceqim  39939  disjorimxrn  39983  disjim  40019  disjlem14  40036  ollat  40473  omlol  40500  cvlatl  40585  hlomcmcv  40616  2dim  40730  1dimN  40731  lcfl8b  42764  lclkrlem2  42792  lclkrslem1  42797  lclkrslem2  42798  lcfrlem9  42810  mapdval2N  42890  mapdordlem2  42897  mapdrvallem2  42905  idomnnzgmulnz  43386  aks6d1c6lem3  43425  readvrec2  43616  readvrec  43617  readvcot  43619  nacsacs  43924  eldiophelnn0  43979  lnmlmod  44285  lnrring  44317  mncply  44342  idomodle  44396  areaquad  44421  dfno2  44632  harval3  44742  alephiso3  44763  mnurndlem1  45468  nznngen  45503  binomcxplemcvg  45541  2uasbanh  45746  relpf  46146  disjinfi  46422  climxrre  46975  mbfdmssre  47225  stoweidlem14  47239  stoweidlem16  47241  stoweidlem24  47249  stoweidlem51  47276  stoweidlem54  47279  etransclem32  47491  sge0fodjrnlem  47641  pimrecltpos  47933  pimrecltneg  47949  smfaddlem1  47988  smflimsuplem7  48051  chnrin  48121  ndmafv  48425  dfafv23  48538  dfatcolem  48540  dfatco  48541  evenz  48943  oddz  48944  gbeeven  49067  gbowodd  49068  sclnbgrisvtx  49162  grlimgredgex  49313  idomcanr  49660  ssnn0ssfz  49676  elbigof  49881  digvalnn0  49926  2sphere  50076  mof0  50164  mof0ALT  50166  uobeq2  50751  thinccat  50772  termcthin  50827  tanhf  51133