Theorem simprbi 500

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

Hypothesis

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

Assertion

Ref	Expression
simprbi	⊢ (𝜑 → 𝜒)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 499	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simplbiim  508  xornan  1516  eumo  2577  reurmo  3330  pssne  3997  pssn2lp  4002  ssnpss  4004  eldifn  4028  elinel2  4096  rabsnt  4633  eldifsni  4689  unimax  4843  ssintub  4863  moop2  5370  pwssun  5436  weso  5527  opelxp2  5578  frpoinsg  6175  wfisg  6183  ordwe  6204  funmo  6374  funopg  6392  funun  6404  fununi  6433  fndm  6459  frn  6530  f1ss  6599  f1ssr  6600  forn  6614  f1f1orn  6650  f1orescnv  6654  f1imacnv  6655  funcocnv2  6663  dffv2  6784  exfo  6902  foelrn  6903  isorel  7113  isoini2  7126  f1ofveu  7186  fovcl  7316  onminesb  7555  onminsb  7556  tfis  7611  limomss  7627  nnlim  7636  ssnlim  7642  curry1  7850  curry2  7853  f1o2ndf1  7869  fnwelem  7876  mpoxopn0yelv  7933  wfrlem5  8037  tz7.48lem  8155  dif20el  8210  oeordi  8293  oeeulem  8307  oeeui  8308  nnawordex  8343  swoer  8399  eceqoveq  8482  mapsnconst  8551  resixpfo  8595  boxcutc  8600  sdomnen  8635  en0  8669  en0OLD  8670  en0ALT  8671  en1  8676  en1OLD  8677  fodomr  8775  dif1enlem  8816  unxpdomlem3  8860  fineqvlem  8868  f1opwfi  8958  fsuppcolem  8995  fsuppco  8996  mapfienlem1  8999  mapfienlem2  9000  supub  9053  suplub  9054  ordtypelem2  9113  ordtypelem3  9114  ordtypelem6  9117  ordtypelem7  9118  wemapso2lem  9146  wdom2d  9174  brwdom3  9176  ixpiunwdom  9184  inf3lem2  9222  inf3lem6  9226  oancom  9244  infdifsn  9250  cantnfp1lem3  9273  cantnflem3  9284  cantnflem4  9285  oef1o  9291  cnfcom3  9297  tctr  9334  tz9.12lem3  9370  scottex  9466  cardid2  9534  infxpenlem  9592  acni3  9626  cardaleph  9668  iscard3  9672  dfac5lem4  9705  dfac5lem5  9706  kmlem1  9729  cofsmo  9848  fin4en1  9888  enfin2i  9900  fin23lem28  9919  fin23lem38  9928  isf32lem6  9937  enfin1ai  9963  hsmexlem2  10006  hsmexlem4  10008  domtriomlem  10021  axdc2lem  10027  axdc3lem2  10030  ac6num  10058  zorn2lem2  10076  brdom3  10107  alephval2  10151  alephreg  10161  pwcfsdom  10162  smobeth  10165  fpwwe2lem5  10214  fpwwe2lem12  10221  canthp1lem2  10232  pwfseqlem3  10239  hargch  10252  winalim2  10275  gchina  10278  inar1  10354  0npi  10461  mulclpi  10472  mulcanpi  10479  nlt1pi  10485  nqereu  10508  prcdnq  10572  prnmax  10574  ltresr2  10720  axrnegex  10741  axpre-sup  10748  eluz2gt1  12481  1nuz2  12485  zsupss  12498  rpgt0  12563  ixxss1  12918  ixxss2  12919  ixxss12  12920  lbioo  12931  ubioo  12932  iccss2  12971  iccssico2  12974  elfzuz3  13074  serge0  13595  expge0  13636  expge1  13637  expaddzlem  13643  hashrabsn1  13906  hashfun  13969  cshinj  14341  relexpuzrel  14580  shftfn  14601  sqrlem6  14776  rlimss  15028  lo1dm  15045  o1dm  15056  rlimrege0  15105  fsumf1o  15252  fsumge0  15322  incexc2  15365  supcvg  15383  fprodf1o  15471  divalglem9  15925  bitsfzolem  15956  bitsf1  15968  gcdcllem1  16021  bezout  16066  nprm  16208  dvdsprm  16223  coprm  16231  dfphi2  16290  phimullem  16295  phisum  16306  expnprm  16418  prmreclem2  16433  prmreclem5  16436  1arith  16443  4sqlem18  16478  vdwnnlem3  16513  ramtlecl  16516  rami  16531  0ram  16536  ramub1lem1  16542  prmgaplem5  16571  acsfiel  17111  isacs1i  17114  catlid  17140  catrid  17141  fullfo  17373  fthf1  17378  fthoppc  17384  invfuc  17437  prslem  17759  posi  17778  tleile  17881  dlatmjdi  17983  pslem  18032  tsrlin  18045  cnvtsr  18048  tsrdir  18064  mndid  18137  mhmf  18177  mhmlin  18179  mhm0  18180  mndind  18208  grpinvex  18329  grplinv  18370  mulgz  18473  mulgdirlem  18476  mulgdir  18477  mulgass  18482  nsgbi  18527  nmzbi  18534  ghmf  18580  ghmlin  18581  conjnsg  18612  gimf1o  18621  gagrpid  18642  gaf  18643  gaass  18645  psgnunilem5  18840  odid  18884  odf1o2  18916  gexid  18924  sylow1lem4  18944  pj1id  19043  efgredeu  19096  ablcmn  19131  cmncom  19141  mulgdi  19166  torsubg  19193  cyggenod2  19223  cygctb  19231  ghmcyg  19235  dprdf1o  19373  ablfacrplem  19406  ablfaclem2  19427  ablfac2  19430  simpg2nsg  19437  fincygsubgodexd  19454  crngmgp  19524  rhmmhm  19696  rhmghm  19699  drngunit  19726  drngmgp  19733  drngid  19735  subrgss  19755  subrg1cl  19762  issubdrg  19779  cntzsdrg  19800  abvge0  19815  srngcnv  19843  lmhmlin  20026  lmimf1o  20054  lvecdrng  20096  lspsolvlem  20133  islbs3  20146  lbsextlem3  20151  2idlcpbl  20226  nzrnz  20252  opprnzr  20257  rrgeq0i  20281  domneq0  20289  domnrrg  20292  drngdomn  20295  fldidom  20297  zringunit  20407  prmirredlem  20413  znidomb  20480  cygzn  20489  psgndiflemB  20516  pjf  20629  frlmsslsp  20712  frlmlbs  20713  f1lindf  20738  assalem  20773  psrbaglefi  20845  mplelsfi  20911  mplsubrglem  20920  mplcoe1  20948  mplbas2  20953  opsrtoslem2  20967  mhpmulcl  21043  coe1mul2  21144  pmatcoe1fsupp  21552  toponuni  21765  tpsuni  21787  mretopd  21943  neips  21964  neiptoptop  21982  neiptopnei  21983  perflp  22005  perfi  22006  cnf  22097  cnpf  22098  cnpimaex  22107  cnima  22116  t0sep  22175  t1ficld  22178  hausnei  22179  pnrmcld  22193  cnrmi  22211  cmpcov  22240  tgcmp  22252  hauscmplem  22257  connclo  22266  1stcclb  22295  2ndcdisj  22307  llyi  22325  nllyi  22326  ptpjpre1  22422  ptpjcn  22462  ptpjopn  22463  ptclsg  22466  dfac14  22469  txdis1cn  22486  pthaus  22489  hauseqlcld  22497  txkgen  22503  xkococn  22511  txconn  22540  hmeocnvcn  22612  fbssfi  22688  filss  22704  uffixfr  22774  flimneiss  22817  flimelbas  22819  flimfnfcls  22879  alexsubb  22897  alexsubALT  22902  ptcmplem2  22904  ptcmplem3  22905  ptcmplem4  22906  tmdgsum2  22947  ghmcnp  22966  tgpt0  22970  qustgplem  22972  istdrg2  23029  vscacn  23037  tvctdrg  23044  uspreg  23125  ucncn  23136  neipcfilu  23147  cuspcvg  23152  psmetxrge0  23165  isxmet2d  23179  prdsxmetlem  23220  imasdsf1olem  23225  xmstopn  23303  mstopn  23304  stdbdxmet  23367  prdsxmslem2  23381  nrgabv  23513  nmvs  23528  nvclvec  23549  nmoge0  23573  nghmcl  23579  nmoi  23580  nghmghm  23586  nmhmlmhm  23601  nmhmnghm  23602  icccmp  23676  xrge0gsumle  23684  metds0  23701  metdstri  23702  metdsre  23704  metdseq0  23705  metdscnlem  23706  metnrmlem1a  23709  icopnfcnv  23793  xrhmeo  23797  pcoval1  23864  cvslvec  23976  cvsunit  23982  cphreccllem  24029  cphsscph  24102  cmetcvg  24136  lmle  24152  cmscmet  24197  cmetcusp1  24204  hlcph  24215  minveclem4  24283  ivthlem3  24304  ovolmge0  24328  ovolicc1  24367  ovolicc2lem3  24370  ovolicc2lem5  24372  dyadmbl  24451  i1ff  24527  i1frn  24528  i1fima2  24530  itg2monolem1  24602  dvnres  24782  c1liplem1  24847  c1lip2  24849  dvge0  24857  lhop1lem  24864  itgsubstlem  24899  fta1glem2  25018  fta1b  25021  plyf  25046  plypf1  25060  plyadd  25065  plymul  25066  coeeu  25073  dgrlem  25077  coeid  25086  elqaalem3  25168  aareccl  25173  eff1olem  25391  relogf1o  25409  logdmn0  25482  logcnlem2  25485  logcnlem3  25486  efopnlem1  25498  efopnlem2  25499  logtayl2  25504  cxpcn3lem  25587  cxpcn3  25588  logbgcd1irr  25631  atandmneg  25743  atandmcj  25746  efiatan2  25754  cosatan  25758  cosatanne0  25759  dvatan  25772  areage0  25800  cxp2lim  25813  jensenlem2  25824  jensen  25825  eldmgm  25858  dmgmaddn0  25859  dmlogdmgm  25860  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem5  25869  lgambdd  25873  lgamucov  25874  ftalem3  25911  efnnfsumcl  25939  efchtdvds  25995  sqff1o  26018  fsumdvdsdiaglem  26019  dvdsppwf1o  26022  dvdsflf1o  26023  musum  26027  muinv  26029  dvdsmulf1o  26030  lgsfle1  26141  lgsle1  26147  lgsdirprm  26166  lgsne0  26170  lgseisenlem3  26212  lgseisenlem4  26213  lgsquadlem1  26215  lgsquadlem2  26216  chebbnd1  26307  chtppilim  26310  chpchtlim  26314  chpo1ub  26315  dchrmusumlema  26328  dchrvmasumlem1  26330  dchrisum0lema  26349  dchrisum0lem2a  26352  logsqvma  26377  selberg3lem2  26393  pntrsumo1  26400  pnt2  26448  ostthlem1  26462  ostth3  26473  axtgcgrrflx  26507  axtgcgrid  26508  axtgsegcon  26509  axtg5seg  26510  axtgbtwnid  26511  axtgpasch  26512  axtgcont1  26513  tglng  26591  axcontlem7  27015  axcontlem10  27018  upgrle  27135  umgredg2  27145  lfgredgge2  27169  usgredg2ALT  27235  usgr1vr  27297  usgrexmpledg  27304  upgrres1  27355  fusgrvtxfi  27361  vtxnbuvtx  27433  cusgrcplgr  27462  vdumgr0  27522  vtxdgoddnumeven  27595  trlres  27742  usgr2pth  27805  cyclispthon  27842  clwwlknlen  28069  clwwnonrepclwwnon  28382  2clwwlk2  28385  ablocom  28583  phpar2  28858  cbncms  28900  hlph  28924  hcaucvg  29221  hlimconvi  29226  shaddcl  29252  shmulcl  29253  chlimi  29269  chcompl  29277  choc1  29362  nmopre  29905  cnopc  29948  lnopl  29949  unop  29950  hmop  29957  cnfnc  29965  lnfnl  29966  nlelshi  30095  cnlnadjlem5  30106  elpjidm  30219  mdslle1i  30352  mdslle2i  30353  atcv0  30377  chpssati  30398  fovcld  30648  aciunf1lem  30673  padct  30728  ssnnssfz  30782  ccatf1  30897  swrdrndisj  30903  ressprs  30914  oduprs  30915  resspos  30917  resstos  30918  pwrssmgc  30951  ogrpinv0le  31014  ogrpsub  31015  ogrpaddlt  31016  cyc3evpm  31090  cycpmgcl  31093  cycpmconjslem2  31095  cyc3conja  31097  isarchi3  31114  archirng  31115  archirngz  31116  archiabllem1a  31118  archiabllem1b  31119  archiabllem2a  31121  archiabllem2c  31122  archiabllem2b  31123  archiabl  31125  orngsqr  31176  ornglmulle  31177  orngrmulle  31178  ofldtos  31183  ofldlt1  31185  ofldchr  31186  suborng  31187  subofld  31188  isarchiofld  31189  nn0omnd  31213  quslsm  31261  nsgmgclem  31264  nsgmgc  31265  prmidl0  31294  qsidomlem1  31296  krull  31311  sradrng  31341  extdg1id  31406  madjusmdetlem4  31448  qtophaus  31454  crefi  31465  cmpcref  31468  cmppcmp  31476  pcmplfin  31478  zart0  31497  tpr2rico  31530  rge0scvg  31567  zrhunitpreima  31594  qqhrhm  31605  esummono  31688  gsumesum  31693  esumrnmpt2  31702  esumpinfval  31707  esumpcvgval  31712  esumpmono  31713  0elsiga  31748  sigaclcu  31751  issgon  31757  inelpisys  31788  ldsysgenld  31794  ldgenpisyslem1  31797  sxuni  31827  isrnmeas  31834  measvuni  31848  measssd  31849  ddemeas  31870  imambfm  31895  elmbfmvol2  31900  dya2icoseg2  31911  omssubaddlem  31932  omssubadd  31933  carsgsigalem  31948  pmeasmono  31957  sibfinima  31972  oddpwdc  31987  oddpwdcv  31988  eulerpartlemf  32003  eulerpartlemt  32004  eulerpartlemr  32007  eulerpartlemgvv  32009  eulerpartlemgs2  32013  fiblem  32031  probtot  32045  ballotlem4  32131  ballotlem5  32132  ballotlemfrc  32159  ballotlemirc  32164  ballotth  32170  hgt750lemb  32302  bnj642  32394  bnj643  32395  bnj645  32396  bnj707  32401  bnj1379  32477  bnj1538  32502  bnj110  32505  bnj93  32510  bnj906  32577  bnj1006  32607  bnj1110  32629  bnj1121  32632  bnj1204  32659  bnj1321  32674  bnj1364  32675  bnj1398  32681  bnj1450  32697  bnj1312  32705  bnj1501  32714  bnj1523  32718  0nn0m1nnn0  32738  subfacp1lem3  32811  subfacp1lem5  32813  pconncn  32853  connpconn  32864  cvmcov  32892  cvmliftlem1  32914  cvmliftlem10  32923  cvmlift2lem11  32942  cvmlift2lem12  32943  msubff1  33185  mvhf1  33188  mthmpps  33211  mclspps  33213  fundmpss  33410  tfisg  33456  frinsg  33462  sltval2  33545  funpartfun  33931  fnetg  34220  neibastop1  34234  filnetlem3  34255  onint1  34324  bj-nnfa  34596  bj-idres  35015  bj-rvecrr  35151  icorempo  35208  pibt2  35274  wl-nfeqfb  35381  phpreu  35447  fin2solem  35449  fin2so  35450  lindsenlbs  35458  matunitlindflem1  35459  matunitlindflem2  35460  matunitlindf  35461  ptrest  35462  poimirlem1  35464  poimirlem2  35465  poimirlem3  35466  poimirlem4  35467  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem9  35472  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem13  35476  poimirlem14  35477  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem24  35487  poimirlem26  35489  poimirlem27  35490  poimirlem29  35492  poimirlem31  35494  mblfinlem2  35501  dvtan  35513  itg2gt0cn  35518  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  cover2  35558  indexa  35577  istotbnd3  35615  sstotbnd2  35618  sstotbnd  35619  totbndss  35621  equivtotbnd  35622  isbnd3  35628  totbndbnd  35633  equivbnd  35634  prdsbnd  35637  prdstotbnd  35638  heibor  35665  zrdivrng  35797  crngocom  35845  isfld2  35849  dmncrng  35900  eqvrelrel  36396  disjrel  36527  prter2  36581  toycom  36673  lsateln0  36695  lpssat  36713  lssat  36716  oposlem  36882  olop  36914  omllaw  36943  cvlexch1  37028  dihpN  39036  mapdordlem2  39337  mhphflem  39935  prjspertr  40093  nacsfg  40171  nacsfix  40178  mzpindd  40212  diophrw  40225  diophrex  40241  rexzrexnn0  40270  pell1234qrdich  40327  rmspecnonsq  40373  rmspecfund  40375  rmspecpos  40382  monotoddzzfi  40408  ltrmxnn0  40415  rmxnn  40417  jm2.23  40462  jm3.1lem2  40484  dnnumch3  40516  lnmlssfg  40549  lnmlmic  40557  lnrlnm  40582  lnr2i  40585  lpirlnr  40586  hbtlem6  40598  hbt  40599  mnccoe  40607  idomrootle  40664  proot1mul  40668  proot1hash  40669  deg1mhm  40676  ntrneifv2  41308  grucollcld  41492  mnurndlem1  41513  ismnushort  41533  radcnvrat  41546  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  ordelordALT  41771  2uasbanh  41795  ordelordALTVD  42101  elixpconstg  42253  rabidim2  42266  foelrnf  42338  disjinfi  42345  supminfxr2  42625  sumnnodd  42789  stoweidlem7  43166  stoweidlem14  43173  stoweidlem16  43175  stoweidlem24  43183  stoweidlem31  43190  stoweidlem54  43213  wallispilem3  43226  fourierdlem42  43308  fourierdlem48  43313  fourierdlem51  43316  fourierdlem64  43329  fourierdlem76  43341  fourierdlem79  43344  fourierdlem81  43346  fourierdlem87  43352  etransclem28  43421  etransclem32  43425  sge0fodjrnlem  43572  hoidmvlelem3  43753  pimrecltpos  43861  pimrecltneg  43875  issmflem  43878  smfaddlem1  43913  smfsuplem1  43959  smfsuplem3  43961  smflimsuplem7  43974  smfliminflem  43978  nfunsnafv  44249  faovcl  44307  tz6.12-2-afv2  44344  tz6.12i-afv2  44350  sprel  44552  evendiv2z  44700  oddp1div2z  44701  2dvdseven  44721  2ndvdsodd  44723  perfectALTVlem1  44789  sbgoldbm  44852  clintopcllaw  45021  0ringbas  45045  rnghmmgmhm  45068  uzlidlring  45103  rnghmsubcsetclem1  45149  rngccatidALTV  45163  zrinitorngc  45174  zrtermorngc  45175  rhmsubcsetclem1  45195  funcringcsetcALTV2lem7  45216  ringccatidALTV  45226  funcringcsetclem7ALTV  45239  irinitoringc  45243  zrtermoringc  45244  fldhmsubc  45258  fldhmsubcALTV  45276  ssnn0ssfz  45301  el0ldepsnzr  45424  regt1loggt0  45498  elbigodm  45517  fllogbd  45522  rrx2xpref1o  45680  unilbss  45779  fdomne0  45793  f002  45797  thincmo2  45925  thincmoALT  45927  fullthinc  45943  elsetrecslem  46018