Theorem simprbi 498

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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 497	1 ⊢ (𝜑 → 𝜒)

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

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 398

This theorem is referenced by:  simplbiim  506  xornan  1519  eumo  2573  reurmo  3380  pssne  4096  pssn2lp  4101  ssnpss  4103  eldifn  4127  elinel2  4196  rabsnt  4735  eldifsni  4793  unimax  4948  ssintub  4970  moop2  5502  pwssun  5571  weso  5667  opelxp2  5718  predpo  6322  frpoinsg  6342  wfisgOLD  6353  ordwe  6375  funmo  6561  funmoOLD  6562  funopg  6580  funun  6592  fununi  6621  funimaexg  6632  fndm  6650  frn  6722  f1ss  6791  f1ssr  6792  forn  6806  f1f1orn  6842  f1orescnv  6846  f1imacnv  6847  funcocnv2  6856  dffv2  6984  exfo  7104  foelrn  7105  isorel  7320  isoini2  7333  f1ofveu  7400  fovcld  7533  onminesb  7778  onminsb  7779  tfisg  7840  tfis  7841  limomss  7857  nnlim  7866  ssnlim  7872  curry1  8087  curry2  8090  f1o2ndf1  8105  fnwelem  8114  mpoxopn0yelv  8195  wfrlem5OLD  8310  tz7.48lem  8438  dif20el  8502  oeordi  8584  oeeulem  8598  oeeui  8599  nnawordex  8634  swoer  8730  eceqoveq  8813  mapsnconst  8883  resixpfo  8927  boxcutc  8932  sdomnen  8974  en0  9010  en0OLD  9011  en0ALT  9012  en0r  9013  en1  9018  en1OLD  9019  dom0  9099  fodomr  9125  dif1enlem  9153  dif1enlemOLD  9154  unxpdomlem3  9249  fineqvlem  9259  infn0  9304  f1opwfi  9353  fsuppcolem  9393  fsuppco  9394  mapfienlem1  9397  mapfienlem2  9398  supub  9451  suplub  9452  ordtypelem2  9511  ordtypelem3  9512  ordtypelem6  9515  ordtypelem7  9516  wemapso2lem  9544  wdom2d  9572  brwdom3  9574  ixpiunwdom  9582  inf3lem2  9621  inf3lem6  9625  oancom  9643  infdifsn  9649  cantnfp1lem3  9672  cantnflem3  9683  cantnflem4  9684  oef1o  9690  cnfcom3  9696  tctr  9732  frinsg  9743  tz9.12lem3  9781  scottex  9877  cardid2  9945  infxpenlem  10005  acni3  10039  cardaleph  10081  iscard3  10085  dfac5lem4  10118  dfac5lem5  10119  kmlem1  10142  cofsmo  10261  fin4en1  10301  enfin2i  10313  fin23lem28  10332  fin23lem38  10341  isf32lem6  10350  enfin1ai  10376  hsmexlem2  10419  hsmexlem4  10421  domtriomlem  10434  axdc2lem  10440  axdc3lem2  10443  ac6num  10471  zorn2lem2  10489  brdom3  10520  alephval2  10564  alephreg  10574  pwcfsdom  10575  smobeth  10578  fpwwe2lem5  10627  fpwwe2lem12  10634  canthp1lem2  10645  pwfseqlem3  10652  hargch  10665  winalim2  10688  gchina  10691  inar1  10767  0npi  10874  mulclpi  10885  mulcanpi  10892  nlt1pi  10898  nqereu  10921  prcdnq  10985  prnmax  10987  ltresr2  11133  axrnegex  11154  axpre-sup  11161  eluz2gt1  12901  1nuz2  12905  zsupss  12918  rpgt0  12983  ixxss1  13339  ixxss2  13340  ixxss12  13341  lbioo  13352  ubioo  13353  iccss2  13392  iccssico2  13395  elfzuz3  13495  serge0  14019  expge0  14061  expge1  14062  expaddzlem  14068  hashrabsn1  14331  hashfun  14394  cshinj  14758  relexpuzrel  14996  shftfn  15017  01sqrexlem6  15191  rlimss  15443  lo1dm  15460  o1dm  15471  rlimrege0  15520  fsumf1o  15666  fsumge0  15738  incexc2  15781  supcvg  15799  fprodf1o  15887  divalglem9  16341  bitsfzolem  16372  bitsf1  16384  gcdcllem1  16437  bezout  16482  nprm  16622  dvdsprm  16637  coprm  16645  dfphi2  16704  phimullem  16709  phisum  16720  expnprm  16832  prmreclem2  16847  prmreclem5  16850  1arith  16857  4sqlem18  16892  vdwnnlem3  16927  ramtlecl  16930  rami  16945  0ram  16950  ramub1lem1  16956  prmgaplem5  16985  acsfiel  17595  isacs1i  17598  catlid  17624  catrid  17625  fullfo  17860  fthf1  17865  fthoppc  17871  invfuc  17924  prslem  18248  posi  18267  tleile  18371  dlatmjdi  18473  pslem  18522  tsrlin  18535  cnvtsr  18538  tsrdir  18554  mndid  18632  mhmf  18674  mhmlin  18676  mhm0  18677  mndind  18706  grpinvex  18826  grplinv  18871  mulgz  18977  mulgdirlem  18980  mulgdir  18981  mulgass  18986  nsgbi  19032  nmzbi  19039  ghmf  19091  ghmlin  19092  conjnsg  19123  gimf1o  19132  gagrpid  19153  gaf  19154  gaass  19156  psgnunilem5  19357  odid  19401  odf1o2  19436  gexid  19444  sylow1lem4  19464  pj1id  19562  efgredeu  19615  ablcmn  19650  cmncom  19661  mulgdi  19689  torsubg  19717  cyggenod2  19748  cygctb  19755  ghmcyg  19759  dprdf1o  19897  ablfacrplem  19930  ablfaclem2  19951  ablfac2  19954  simpg2nsg  19961  fincygsubgodexd  19978  crngmgp  20058  rhmmhm  20251  rhmghm  20255  rimf1o  20265  nzrnz  20287  opprnzr  20292  drngunit  20313  fldcrngd  20321  drngmgp  20324  drngid  20326  subrgss  20357  subrg1cl  20364  issubdrg  20382  fldsdrgfld  20407  cntzsdrg  20411  abvge0  20426  srngcnv  20454  lmhmlin  20639  lmimf1o  20667  lvecdrng  20709  lspsolvlem  20748  islbs3  20761  lbsextlem3  20766  2idlelbas  20863  2idlcpbl  20864  rrgeq0i  20898  domneq0  20906  domnrrg  20909  drngdomn  20914  fldidomOLD  20917  zringunit  21028  prmirredlem  21034  znidomb  21109  cygzn  21118  psgndiflemB  21145  pjf  21260  frlmsslsp  21343  frlmlbs  21344  f1lindf  21369  assalem  21404  psrbaglefi  21477  mplelsfi  21546  mplsubrglem  21555  mplcoe1  21584  mplbas2  21589  opsrtoslem2  21609  mhpmulcl  21684  coe1mul2  21783  pmatcoe1fsupp  22195  toponuni  22408  tpsuni  22430  mretopd  22588  neips  22609  neiptoptop  22627  neiptopnei  22628  perflp  22650  perfi  22651  cnf  22742  cnpf  22743  cnpimaex  22752  cnima  22761  t0sep  22820  t1ficld  22823  hausnei  22824  pnrmcld  22838  cnrmi  22856  cmpcov  22885  tgcmp  22897  hauscmplem  22902  connclo  22911  1stcclb  22940  2ndcdisj  22952  llyi  22970  nllyi  22971  ptpjpre1  23067  ptpjcn  23107  ptpjopn  23108  ptclsg  23111  dfac14  23114  txdis1cn  23131  pthaus  23134  hauseqlcld  23142  txkgen  23148  xkococn  23156  txconn  23185  hmeocnvcn  23257  fbssfi  23333  filss  23349  uffixfr  23419  flimneiss  23462  flimelbas  23464  flimfnfcls  23524  alexsubb  23542  alexsubALT  23547  ptcmplem2  23549  ptcmplem3  23550  ptcmplem4  23551  tmdgsum2  23592  ghmcnp  23611  tgpt0  23615  qustgplem  23617  istdrg2  23674  vscacn  23682  tvctdrg  23689  uspreg  23771  ucncn  23782  neipcfilu  23793  cuspcvg  23798  psmetxrge0  23811  isxmet2d  23825  prdsxmetlem  23866  imasdsf1olem  23871  xmstopn  23949  mstopn  23950  stdbdxmet  24016  prdsxmslem2  24030  nrgabv  24170  nmvs  24185  nvclvec  24206  nmoge0  24230  nghmcl  24236  nmoi  24237  nghmghm  24243  nmhmlmhm  24258  nmhmnghm  24259  icccmp  24333  xrge0gsumle  24341  metds0  24358  metdstri  24359  metdsre  24361  metdseq0  24362  metdscnlem  24363  metnrmlem1a  24366  icopnfcnv  24450  xrhmeo  24454  pcoval1  24521  cvslvec  24633  cvsunit  24639  recvs  24654  cphreccllem  24687  cphsscph  24760  cmetcvg  24794  lmle  24810  cmscmet  24855  cmetcusp1  24862  hlcph  24873  minveclem4  24941  ivthlem3  24962  ovolmge0  24986  ovolicc1  25025  ovolicc2lem3  25028  ovolicc2lem5  25030  dyadmbl  25109  i1ff  25185  i1frn  25186  i1fima2  25188  itg2monolem1  25260  dvnres  25440  c1liplem1  25505  c1lip2  25507  dvge0  25515  lhop1lem  25522  itgsubstlem  25557  fta1glem2  25676  fta1b  25679  plyf  25704  plypf1  25718  plyadd  25723  plymul  25724  coeeu  25731  dgrlem  25735  coeid  25744  elqaalem3  25826  aareccl  25831  eff1olem  26049  relogf1o  26067  logdmn0  26140  logcnlem2  26143  logcnlem3  26144  efopnlem1  26156  efopnlem2  26157  logtayl2  26162  cxpcn3lem  26245  cxpcn3  26246  logbgcd1irr  26289  atandmneg  26401  atandmcj  26404  efiatan2  26412  cosatan  26416  cosatanne0  26417  dvatan  26430  areage0  26458  cxp2lim  26471  jensenlem2  26482  jensen  26483  eldmgm  26516  dmgmaddn0  26517  dmlogdmgm  26518  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem5  26527  lgambdd  26531  lgamucov  26532  ftalem3  26569  efnnfsumcl  26597  efchtdvds  26653  sqff1o  26676  fsumdvdsdiaglem  26677  dvdsppwf1o  26680  dvdsflf1o  26681  musum  26685  muinv  26687  dvdsmulf1o  26688  lgsfle1  26799  lgsle1  26805  lgsdirprm  26824  lgsne0  26828  lgseisenlem3  26870  lgseisenlem4  26871  lgsquadlem1  26873  lgsquadlem2  26874  chebbnd1  26965  chtppilim  26968  chpchtlim  26972  chpo1ub  26973  dchrmusumlema  26986  dchrvmasumlem1  26988  dchrisum0lema  27007  dchrisum0lem2a  27010  logsqvma  27035  selberg3lem2  27051  pntrsumo1  27058  pnt2  27106  ostthlem1  27120  ostth3  27131  sltval2  27149  addsproplem2  27444  sleadd1  27462  negsid  27505  precsexlem8  27650  precsexlem9  27651  precsexlem11  27653  axtgcgrrflx  27703  axtgcgrid  27704  axtgsegcon  27705  axtg5seg  27706  axtgbtwnid  27707  axtgpasch  27708  axtgcont1  27709  tglng  27787  axcontlem7  28218  axcontlem10  28221  upgrle  28340  umgredg2  28350  lfgredgge2  28374  usgredg2ALT  28440  usgr1vr  28502  usgrexmpledg  28509  upgrres1  28560  fusgrvtxfi  28566  vtxnbuvtx  28638  cusgrcplgr  28667  vdumgr0  28727  vtxdgoddnumeven  28800  trlres  28947  usgr2pth  29011  cyclispthon  29048  clwwlknlen  29275  clwwnonrepclwwnon  29588  2clwwlk2  29591  ablocom  29789  phpar2  30064  cbncms  30106  hlph  30130  hcaucvg  30427  hlimconvi  30432  shaddcl  30458  shmulcl  30459  chlimi  30475  chcompl  30483  choc1  30568  nmopre  31111  cnopc  31154  lnopl  31155  unop  31156  hmop  31163  cnfnc  31171  lnfnl  31172  nlelshi  31301  cnlnadjlem5  31312  elpjidm  31425  mdslle1i  31558  mdslle2i  31559  atcv0  31583  chpssati  31604  aciunf1lem  31875  padct  31932  ssnnssfz  31986  ccatf1  32103  swrdrndisj  32109  ressprs  32121  oduprs  32122  resspos  32124  resstos  32125  pwrssmgc  32158  ogrpinv0le  32221  ogrpsub  32222  ogrpaddlt  32223  cyc3evpm  32297  cycpmgcl  32300  cycpmconjslem2  32302  cyc3conja  32304  isarchi3  32321  archirng  32322  archirngz  32323  archiabllem1a  32325  archiabllem1b  32326  archiabllem2a  32328  archiabllem2c  32329  archiabllem2b  32330  archiabl  32332  isdrng4  32384  orngsqr  32411  ornglmulle  32412  orngrmulle  32413  ofldtos  32418  ofldlt1  32420  ofldchr  32421  suborng  32422  subofld  32423  isarchiofld  32424  nn0omnd  32449  quslsm  32505  nsgmgclem  32511  nsgmgc  32512  prmidl0  32558  qsidomlem1  32560  mxidlirred  32577  krull  32583  sradrng  32662  extdg1id  32731  ply1annnr  32753  madjusmdetlem4  32799  qtophaus  32805  crefi  32816  cmpcref  32819  cmppcmp  32827  pcmplfin  32829  zart0  32848  tpr2rico  32881  rge0scvg  32918  zrhunitpreima  32947  qqhrhm  32958  esummono  33041  gsumesum  33046  esumrnmpt2  33055  esumpinfval  33060  esumpcvgval  33065  esumpmono  33066  0elsiga  33101  sigaclcu  33104  issgon  33110  inelpisys  33141  ldsysgenld  33147  ldgenpisyslem1  33150  sxuni  33180  isrnmeas  33187  measvuni  33201  measssd  33202  ddemeas  33223  imambfm  33250  elmbfmvol2  33255  dya2icoseg2  33266  omssubaddlem  33287  omssubadd  33288  carsgsigalem  33303  pmeasmono  33312  sibfinima  33327  oddpwdc  33342  oddpwdcv  33343  eulerpartlemf  33358  eulerpartlemt  33359  eulerpartlemr  33362  eulerpartlemgvv  33364  eulerpartlemgs2  33368  fiblem  33386  probtot  33400  ballotlem4  33486  ballotlem5  33487  ballotlemfrc  33514  ballotlemirc  33519  ballotth  33525  hgt750lemb  33657  bnj642  33748  bnj643  33749  bnj645  33750  bnj707  33755  bnj1379  33830  bnj1538  33855  bnj110  33858  bnj93  33863  bnj906  33930  bnj1006  33960  bnj1110  33982  bnj1121  33985  bnj1204  34012  bnj1321  34027  bnj1364  34028  bnj1398  34034  bnj1450  34050  bnj1312  34058  bnj1501  34067  bnj1523  34071  0nn0m1nnn0  34091  subfacp1lem3  34162  subfacp1lem5  34164  pconncn  34204  connpconn  34215  cvmcov  34243  cvmliftlem1  34265  cvmliftlem10  34274  cvmlift2lem11  34293  cvmlift2lem12  34294  msubff1  34536  mvhf1  34539  mthmpps  34562  mclspps  34564  fundmpss  34727  funpartfun  34904  fnetg  35219  neibastop1  35233  filnetlem3  35254  onint1  35323  bj-nnfa  35595  bj-idres  36030  bj-rvecrr  36167  icorempo  36221  pibt2  36287  wl-nfeqfb  36394  phpreu  36461  fin2solem  36463  fin2so  36464  lindsenlbs  36472  matunitlindflem1  36473  matunitlindflem2  36474  matunitlindf  36475  ptrest  36476  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem4  36481  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem9  36486  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem13  36490  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem23  36500  poimirlem24  36501  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem31  36508  mblfinlem2  36515  dvtan  36527  itg2gt0cn  36532  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  cover2  36572  indexa  36590  istotbnd3  36628  sstotbnd2  36631  sstotbnd  36632  totbndss  36634  equivtotbnd  36635  isbnd3  36641  totbndbnd  36646  equivbnd  36647  prdsbnd  36650  prdstotbnd  36651  heibor  36678  zrdivrng  36810  crngocom  36858  isfld2  36862  dmncrng  36913  eqvrelrel  37456  disjrel  37589  disjdmqscossss  37662  prter2  37740  toycom  37832  lsateln0  37854  lpssat  37872  lssat  37875  oposlem  38041  olop  38073  omllaw  38102  cvlexch1  38187  dihpN  40196  mapdordlem2  40497  mhphflem  41166  prjspertr  41344  nacsfg  41429  nacsfix  41436  mzpindd  41470  diophrw  41483  diophrex  41499  rexzrexnn0  41528  pell1234qrdich  41585  rmspecnonsq  41631  rmspecfund  41633  rmspecpos  41641  monotoddzzfi  41667  ltrmxnn0  41674  rmxnn  41676  jm2.23  41721  jm3.1lem2  41743  dnnumch3  41775  lnmlssfg  41808  lnmlmic  41816  lnrlnm  41841  lnr2i  41844  lpirlnr  41845  hbtlem6  41857  hbt  41858  mnccoe  41866  idomrootle  41923  proot1mul  41927  proot1hash  41928  deg1mhm  41935  ondif1i  41998  limnsuc  42001  cantnfresb  42060  succlg  42064  ntrneifv2  42817  grucollcld  43005  mnurndlem1  43026  ismnushort  43046  radcnvrat  43059  binomcxplemdvbinom  43098  binomcxplemcvg  43099  binomcxplemnotnn0  43101  ordelordALT  43284  2uasbanh  43308  ordelordALTVD  43614  elixpconstg  43764  rabidim2  43777  foelrnf  43870  disjinfi  43877  supminfxr2  44166  sumnnodd  44333  stoweidlem7  44710  stoweidlem14  44717  stoweidlem16  44719  stoweidlem24  44727  stoweidlem31  44734  stoweidlem54  44757  wallispilem3  44770  fourierdlem42  44852  fourierdlem48  44857  fourierdlem51  44860  fourierdlem64  44873  fourierdlem76  44885  fourierdlem79  44888  fourierdlem81  44890  fourierdlem87  44896  etransclem28  44965  etransclem32  44969  sge0fodjrnlem  45119  hoidmvlelem3  45300  ovolval5lem3  45357  pimrecltpos  45411  pimrecltneg  45427  issmflem  45430  smfaddlem1  45466  smfsuplem1  45514  smfsuplem3  45516  smflimsuplem7  45529  smfliminflem  45533  tworepnotupword  45587  nfunsnafv  45837  faovcl  45895  tz6.12-2-afv2  45932  tz6.12i-afv2  45938  sprel  46139  evendiv2z  46287  oddp1div2z  46288  2dvdseven  46308  2ndvdsodd  46310  perfectALTVlem1  46376  sbgoldbm  46439  clintopcllaw  46608  0ringbas  46632  rnghmmgmhm  46678  2idlcpblrng  46748  uzlidlring  46781  rnghmsubcsetclem1  46827  rngccatidALTV  46841  zrinitorngc  46852  zrtermorngc  46853  rhmsubcsetclem1  46873  ringcinv  46884  funcringcsetcALTV2lem7  46894  ringccatidALTV  46904  ringcinvALTV  46908  funcringcsetclem7ALTV  46917  irinitoringc  46921  zrtermoringc  46922  fldhmsubc  46936  fldhmsubcALTV  46954  ssnn0ssfz  46979  el0ldepsnzr  47102  regt1loggt0  47176  elbigodm  47195  fllogbd  47200  rrx2xpref1o  47358  unilbss  47456  fdomne0  47470  f002  47474  thincmo2  47602  thincmoALT  47604  fullthinc  47620  elsetrecslem  47698