Theorem simprbi 496

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  simplbiim  504  xornan  1519  eumo  2578  reurmo  3383  pssne  4099  pssn2lp  4104  ssnpss  4106  eldifn  4132  elinel2  4202  rabsnt  4731  eldifsni  4790  unimax  4944  ssintub  4966  moop2  5507  pwssun  5575  weso  5676  opelxp2  5728  predpo  6344  frpoinsg  6364  wfisgOLD  6375  ordwe  6397  funmo  6581  funmoOLD  6582  funopg  6600  funun  6612  fununi  6641  funimaexg  6653  fndm  6671  frn  6743  f1ss  6809  f1ssr  6810  forn  6823  f1f1orn  6859  f1orescnv  6863  f1imacnv  6864  funcocnv2  6873  dffv2  7004  exfo  7125  foelrn  7127  foelrnf  7128  isorel  7346  isoini2  7359  f1ofveu  7425  fovcld  7560  onminesb  7813  onminsb  7814  tfisg  7875  tfis  7876  limomss  7892  nnlim  7901  ssnlim  7907  resf1ext2b  7957  curry1  8129  curry2  8132  f1o2ndf1  8147  fnwelem  8156  mpoxopn0yelv  8238  wfrlem5OLD  8353  tz7.48lem  8481  dif20el  8543  oeordi  8625  oeeulem  8639  oeeui  8640  nnawordex  8675  swoer  8776  eceqoveq  8862  mapsnconst  8932  resixpfo  8976  boxcutc  8981  sdomnen  9021  en0  9058  en0ALT  9059  en0r  9060  en1  9064  dom0  9142  fodomr  9168  dif1enlem  9196  dif1enlemOLD  9197  unxpdomlem3  9288  fineqvlem  9298  infn0  9340  fodomfir  9368  f1opwfi  9396  fsuppcolem  9441  fsuppco  9442  mapfienlem1  9445  mapfienlem2  9446  supub  9499  suplub  9500  ordtypelem2  9559  ordtypelem3  9560  ordtypelem6  9563  ordtypelem7  9564  wemapso2lem  9592  wdom2d  9620  brwdom3  9622  ixpiunwdom  9630  inf3lem2  9669  inf3lem6  9673  oancom  9691  infdifsn  9697  cantnfp1lem3  9720  cantnflem3  9731  cantnflem4  9732  oef1o  9738  cnfcom3  9744  tctr  9780  frinsg  9791  tz9.12lem3  9829  scottex  9925  cardid2  9993  infxpenlem  10053  acni3  10087  cardaleph  10129  iscard3  10133  dfac5lem4  10166  dfac5lem5  10167  dfac5lem4OLD  10168  kmlem1  10191  cofsmo  10309  fin4en1  10349  enfin2i  10361  fin23lem28  10380  fin23lem38  10389  isf32lem6  10398  enfin1ai  10424  hsmexlem2  10467  hsmexlem4  10469  domtriomlem  10482  axdc2lem  10488  axdc3lem2  10491  ac6num  10519  zorn2lem2  10537  brdom3  10568  alephval2  10612  alephreg  10622  pwcfsdom  10623  smobeth  10626  fpwwe2lem5  10675  fpwwe2lem12  10682  canthp1lem2  10693  pwfseqlem3  10700  hargch  10713  winalim2  10736  gchina  10739  inar1  10815  0npi  10922  mulclpi  10933  mulcanpi  10940  nlt1pi  10946  nqereu  10969  prcdnq  11033  prnmax  11035  ltresr2  11181  axrnegex  11202  axpre-sup  11209  eluz2gt1  12962  1nuz2  12966  zsupss  12979  rpgt0  13047  ixxss1  13405  ixxss2  13406  ixxss12  13407  lbioo  13418  ubioo  13419  iccss2  13458  iccssico2  13461  elfzuz3  13561  serge0  14097  expge0  14139  expge1  14140  expaddzlem  14146  hashrabsn1  14413  hashfun  14476  cshinj  14849  relexpuzrel  15091  shftfn  15112  01sqrexlem6  15286  rlimss  15538  lo1dm  15555  o1dm  15566  rlimrege0  15615  fsumf1o  15759  fsumge0  15831  incexc2  15874  supcvg  15892  fprodf1o  15982  divalglem9  16438  bitsfzolem  16471  bitsf1  16483  gcdcllem1  16536  bezout  16580  nprm  16725  dvdsprm  16740  coprm  16748  dfphi2  16811  phimullem  16816  phisum  16828  expnprm  16940  prmreclem2  16955  prmreclem5  16958  1arith  16965  4sqlem18  17000  vdwnnlem3  17035  ramtlecl  17038  rami  17053  0ram  17058  ramub1lem1  17064  prmgaplem5  17093  acsfiel  17697  isacs1i  17700  catlid  17726  catrid  17727  fullfo  17959  fthf1  17964  fthoppc  17970  invfuc  18022  prslem  18343  oduprs  18346  posi  18363  tleile  18466  dlatmjdi  18568  pslem  18617  tsrlin  18630  cnvtsr  18633  tsrdir  18649  mndid  18757  mhmf  18802  mhmlin  18806  mhm0  18807  mndind  18841  grpinvex  18961  grplinv  19007  mulgz  19120  mulgdirlem  19123  mulgdir  19124  mulgass  19129  nsgbi  19175  nmzbi  19182  ghmf  19238  ghmlin  19239  conjnsg  19272  gimf1o  19281  gagrpid  19312  gaf  19313  gaass  19315  psgnunilem5  19512  odid  19556  odf1o2  19591  gexid  19599  sylow1lem4  19619  pj1id  19717  efgredeu  19770  ablcmn  19805  cmncom  19816  mulgdi  19844  torsubg  19872  cyggenod2  19903  cygctb  19910  ghmcyg  19914  dprdf1o  20052  ablfacrplem  20085  ablfaclem2  20106  ablfac2  20109  simpg2nsg  20116  fincygsubgodexd  20133  crngmgp  20238  rnghmmgmhm  20443  rhmmhm  20479  rhmghm  20484  rimf1o  20494  nzrnz  20515  0ringbas  20528  subrgss  20572  subrg1cl  20580  rnghmsubcsetclem1  20631  zrinitorngc  20642  zrtermorngc  20643  rhmsubcsetclem1  20660  ringcinv  20671  zrtermoringc  20675  rrgeq0i  20699  domneq0  20708  domnrrg  20713  drngunit  20734  fldcrngd  20742  drngmgp  20745  drngid  20746  drngdomn  20749  fldidomOLD  20772  issubdrg  20781  fldhmsubc  20786  fldsdrgfld  20799  cntzsdrg  20803  abvge0  20818  srngcnv  20848  lmhmlin  21034  lmimf1o  21062  lvecdrng  21104  lspsolvlem  21144  islbs3  21157  lbsextlem3  21162  2idlelbas  21274  2idlcpblrng  21281  zringunit  21477  prmirredlem  21483  irinitoringc  21490  znidomb  21580  cygzn  21589  psgndiflemB  21618  pjf  21733  frlmsslsp  21816  frlmlbs  21817  f1lindf  21842  assalem  21877  psrbaglefi  21946  psrbagleadd1  21948  mplelsfi  22015  mplsubrglem  22024  mplcoe1  22055  mplbas2  22060  opsrtoslem2  22080  mhpmulcl  22153  psdmul  22170  coe1mul2  22272  pmatcoe1fsupp  22707  toponuni  22920  tpsuni  22942  mretopd  23100  neips  23121  neiptoptop  23139  neiptopnei  23140  perflp  23162  perfi  23163  cnf  23254  cnpf  23255  cnpimaex  23264  cnima  23273  t0sep  23332  t1ficld  23335  hausnei  23336  pnrmcld  23350  cnrmi  23368  cmpcov  23397  tgcmp  23409  hauscmplem  23414  connclo  23423  1stcclb  23452  2ndcdisj  23464  llyi  23482  nllyi  23483  ptpjpre1  23579  ptpjcn  23619  ptpjopn  23620  ptclsg  23623  dfac14  23626  txdis1cn  23643  pthaus  23646  hauseqlcld  23654  txkgen  23660  xkococn  23668  txconn  23697  hmeocnvcn  23769  fbssfi  23845  filss  23861  uffixfr  23931  flimneiss  23974  flimelbas  23976  flimfnfcls  24036  alexsubb  24054  alexsubALT  24059  ptcmplem2  24061  ptcmplem3  24062  ptcmplem4  24063  tmdgsum2  24104  ghmcnp  24123  tgpt0  24127  qustgplem  24129  istdrg2  24186  vscacn  24194  tvctdrg  24201  uspreg  24283  ucncn  24294  neipcfilu  24305  cuspcvg  24310  psmetxrge0  24323  isxmet2d  24337  prdsxmetlem  24378  imasdsf1olem  24383  xmstopn  24461  mstopn  24462  stdbdxmet  24528  prdsxmslem2  24542  nrgabv  24682  nmvs  24697  nvclvec  24718  nmoge0  24742  nghmcl  24748  nmoi  24749  nghmghm  24755  nmhmlmhm  24770  nmhmnghm  24771  icccmp  24847  xrge0gsumle  24855  metds0  24872  metdstri  24873  metdsre  24875  metdseq0  24876  metdscnlem  24877  metnrmlem1a  24880  icopnfcnv  24973  xrhmeo  24977  pcoval1  25046  cvslvec  25158  cvsunit  25164  recvs  25179  cphreccllem  25212  cphsscph  25285  cmetcvg  25319  lmle  25335  cmscmet  25380  cmetcusp1  25387  hlcph  25398  minveclem4  25466  ivthlem3  25488  ovolmge0  25512  ovolicc1  25551  ovolicc2lem3  25554  ovolicc2lem5  25556  dyadmbl  25635  i1ff  25711  i1frn  25712  i1fima2  25714  itg2monolem1  25785  dvnres  25967  c1liplem1  26035  c1lip2  26037  dvge0  26045  lhop1lem  26052  itgsubstlem  26089  fta1glem2  26208  fta1b  26211  idomrootle  26212  plyf  26237  plypf1  26251  plyadd  26256  plymul  26257  coeeu  26264  dgrlem  26268  coeid  26277  elqaalem3  26363  aareccl  26368  eff1olem  26590  relogf1o  26608  logdmn0  26682  logcnlem2  26685  logcnlem3  26686  efopnlem1  26698  efopnlem2  26699  logtayl2  26704  cxpcn3lem  26790  cxpcn3  26791  logbgcd1irr  26837  atandmneg  26949  atandmcj  26952  efiatan2  26960  cosatan  26964  cosatanne0  26965  dvatan  26978  areage0  27006  cxp2lim  27020  jensenlem2  27031  jensen  27032  eldmgm  27065  dmgmaddn0  27066  dmlogdmgm  27067  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgambdd  27080  lgamucov  27081  ftalem3  27118  efnnfsumcl  27146  efchtdvds  27202  sqff1o  27225  fsumdvdsdiaglem  27226  dvdsppwf1o  27229  dvdsflf1o  27230  musum  27234  muinv  27236  mpodvdsmulf1o  27237  dvdsmulf1o  27239  lgsfle1  27350  lgsle1  27356  lgsdirprm  27375  lgsne0  27379  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  chebbnd1  27516  chtppilim  27519  chpchtlim  27523  chpo1ub  27524  dchrmusumlema  27537  dchrvmasumlem1  27539  dchrisum0lema  27558  dchrisum0lem2a  27561  logsqvma  27586  selberg3lem2  27602  pntrsumo1  27609  pnt2  27657  ostthlem1  27671  ostth3  27682  sltval2  27701  addsproplem2  28003  sleadd1  28022  negsid  28073  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  elons2  28281  sltonold  28283  onscutleft  28285  axtgcgrrflx  28470  axtgcgrid  28471  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgcont1  28476  tglng  28554  axcontlem7  28985  axcontlem10  28988  upgrle  29107  umgredg2  29117  lfgredgge2  29141  usgredg2ALT  29210  usgr1vr  29272  usgrexmpledg  29279  upgrres1  29330  fusgrvtxfi  29336  vtxnbuvtx  29408  cusgrcplgr  29437  vdumgr0  29498  vtxdgoddnumeven  29571  trlres  29718  usgr2pth  29784  cyclispthon  29824  clwwlknlen  30051  clwwnonrepclwwnon  30364  2clwwlk2  30367  ablocom  30567  phpar2  30842  cbncms  30884  hlph  30908  hcaucvg  31205  hlimconvi  31210  shaddcl  31236  shmulcl  31237  chlimi  31253  chcompl  31261  choc1  31346  nmopre  31889  cnopc  31932  lnopl  31933  unop  31934  hmop  31941  cnfnc  31949  lnfnl  31950  nlelshi  32079  cnlnadjlem5  32090  elpjidm  32203  mdslle1i  32336  mdslle2i  32337  atcv0  32361  chpssati  32382  aciunf1lem  32672  padct  32731  ssnnssfz  32789  ccatf1  32933  swrdrndisj  32942  ressprs  32954  resspos  32956  resstos  32957  pwrssmgc  32990  ogrpinv0le  33092  ogrpsub  33093  ogrpaddlt  33094  wrdpmtrlast  33113  cyc3evpm  33170  cycpmgcl  33173  cycpmconjslem2  33175  cyc3conja  33177  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1a  33198  archiabllem1b  33199  archiabllem2a  33201  archiabllem2c  33202  archiabllem2b  33203  archiabl  33205  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrun  33253  isdrng4  33298  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ofldtos  33341  ofldlt1  33343  ofldchr  33344  suborng  33345  subofld  33346  isarchiofld  33347  nn0omnd  33373  quslsm  33433  nsgmgclem  33439  nsgmgc  33440  prmidl0  33478  qsidomlem1  33480  mxidlirred  33500  krull  33507  ufdprmidl  33569  1arithufdlem4  33575  sradrng  33633  extdg1id  33716  ply1annnr  33746  madjusmdetlem4  33829  qtophaus  33835  crefi  33846  cmpcref  33849  cmppcmp  33857  pcmplfin  33859  zart0  33878  tpr2rico  33911  rge0scvg  33948  zrhunitpreima  33977  qqhrhm  33990  esummono  34055  gsumesum  34060  esumrnmpt2  34069  esumpinfval  34074  esumpcvgval  34079  esumpmono  34080  0elsiga  34115  sigaclcu  34118  issgon  34124  inelpisys  34155  ldsysgenld  34161  ldgenpisyslem1  34164  sxuni  34194  isrnmeas  34201  measvuni  34215  measssd  34216  ddemeas  34237  imambfm  34264  elmbfmvol2  34269  dya2icoseg2  34280  omssubaddlem  34301  omssubadd  34302  carsgsigalem  34317  pmeasmono  34326  sibfinima  34341  oddpwdc  34356  oddpwdcv  34357  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartlemr  34376  eulerpartlemgvv  34378  eulerpartlemgs2  34382  fiblem  34400  probtot  34414  ballotlem4  34501  ballotlem5  34502  ballotlemfrc  34529  ballotlemirc  34534  ballotth  34540  hgt750lemb  34671  bnj642  34762  bnj643  34763  bnj645  34764  bnj707  34769  bnj1379  34844  bnj1538  34869  bnj110  34872  bnj93  34877  bnj906  34944  bnj1006  34974  bnj1110  34996  bnj1121  34999  bnj1204  35026  bnj1321  35041  bnj1364  35042  bnj1398  35048  bnj1450  35064  bnj1312  35072  bnj1501  35081  bnj1523  35085  0nn0m1nnn0  35118  subfacp1lem3  35187  subfacp1lem5  35189  pconncn  35229  connpconn  35240  cvmcov  35268  cvmliftlem1  35290  cvmliftlem10  35299  cvmlift2lem11  35318  cvmlift2lem12  35319  msubff1  35561  mvhf1  35564  mthmpps  35587  mclspps  35589  fundmpss  35767  funpartfun  35944  fnetg  36346  neibastop1  36360  filnetlem3  36381  onint1  36450  weiunlem2  36464  weiunpo  36466  weiunse  36469  bj-nnfa  36729  bj-idres  37161  bj-rvecrr  37298  icorempo  37352  pibt2  37418  wl-nfeqfb  37537  phpreu  37611  fin2solem  37613  fin2so  37614  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  ptrest  37626  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  dvtan  37677  itg2gt0cn  37682  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  cover2  37722  indexa  37740  istotbnd3  37778  sstotbnd2  37781  sstotbnd  37782  totbndss  37784  equivtotbnd  37785  isbnd3  37791  totbndbnd  37796  equivbnd  37797  prdsbnd  37800  prdstotbnd  37801  heibor  37828  zrdivrng  37960  crngocom  38008  isfld2  38012  dmncrng  38063  eqvrelrel  38598  disjrel  38731  disjdmqscossss  38804  prter2  38882  toycom  38974  lsateln0  38996  lpssat  39014  lssat  39017  oposlem  39183  olop  39215  omllaw  39244  cvlexch1  39329  dihpN  41338  mapdordlem2  41639  linvh  42097  idomnnzpownz  42133  idomnnzgmulnz  42134  aks6d1c5lem2  42139  deg1pow  42142  redvmptabs  42390  readvrec2  42391  readvrec  42392  mhphflem  42606  prjspertr  42615  nacsfg  42716  nacsfix  42723  mzpindd  42757  diophrw  42770  diophrex  42786  rexzrexnn0  42815  pell1234qrdich  42872  rmspecnonsq  42918  rmspecfund  42920  rmspecpos  42928  monotoddzzfi  42954  ltrmxnn0  42961  rmxnn  42963  jm2.23  43008  jm3.1lem2  43030  dnnumch3  43059  lnmlssfg  43092  lnmlmic  43100  lnrlnm  43125  lnr2i  43128  lpirlnr  43129  hbtlem6  43141  hbt  43142  mnccoe  43150  proot1mul  43206  proot1hash  43207  deg1mhm  43212  ondif1i  43275  limnsuc  43278  cantnfresb  43337  succlg  43341  ntrneifv2  44093  grucollcld  44279  mnurndlem1  44300  ismnushort  44320  radcnvrat  44333  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  ordelordALT  44557  2uasbanh  44581  ordelordALTVD  44887  relprel  44972  elixpconstg  45094  rabidim2  45107  disjinfi  45197  supminfxr2  45480  sumnnodd  45645  stoweidlem7  46022  stoweidlem14  46029  stoweidlem16  46031  stoweidlem24  46039  stoweidlem31  46046  stoweidlem54  46069  wallispilem3  46082  fourierdlem42  46164  fourierdlem48  46169  fourierdlem51  46172  fourierdlem64  46185  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem87  46208  etransclem28  46277  etransclem32  46281  sge0fodjrnlem  46431  hoidmvlelem3  46612  ovolval5lem3  46669  pimrecltpos  46723  pimrecltneg  46739  issmflem  46742  smfaddlem1  46778  smfsuplem1  46826  smfsuplem3  46828  smflimsuplem7  46841  smfliminflem  46845  tworepnotupword  46901  nfunsnafv  47154  faovcl  47212  tz6.12-2-afv2  47249  tz6.12i-afv2  47255  sprel  47471  evendiv2z  47619  oddp1div2z  47620  2dvdseven  47640  2ndvdsodd  47642  perfectALTVlem1  47708  sbgoldbm  47771  uhgrimisgrgric  47899  clintopcllaw  48127  uzlidlring  48151  rngccatidALTV  48188  funcringcsetcALTV2lem7  48212  ringccatidALTV  48222  ringcinvALTV  48226  funcringcsetclem7ALTV  48235  fldhmsubcALTV  48249  ssnn0ssfz  48265  el0ldepsnzr  48384  regt1loggt0  48457  elbigodm  48476  fllogbd  48481  rrx2xpref1o  48639  unilbss  48737  fdomne0  48759  f002  48763  thincmo2  49076  thincmoALT  49078  fullthinc  49099  elsetrecslem  49218