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  2572  reurmo  3359  pssne  4065  pssn2lp  4070  ssnpss  4072  eldifn  4098  elinel2  4168  rabsnt  4698  eldifsni  4757  unimax  4911  ssintub  4933  moop2  5465  pwssun  5533  weso  5632  opelxp2  5684  predpo  6299  frpoinsg  6319  ordwe  6348  funmo  6534  funmoOLD  6535  funopg  6553  funun  6565  fununi  6594  funimaexg  6606  fndm  6624  frn  6698  f1ss  6764  f1ssr  6765  forn  6778  f1f1orn  6814  f1orescnv  6818  f1imacnv  6819  funcocnv2  6828  dffv2  6959  exfo  7080  foelrn  7082  foelrnf  7083  isorel  7304  isoini2  7317  f1ofveu  7384  fovcld  7519  onminesb  7772  onminsb  7773  tfisg  7833  tfis  7834  limomss  7850  nnlim  7859  ssnlim  7865  resf1ext2b  7914  curry1  8086  curry2  8089  f1o2ndf1  8104  fnwelem  8113  mpoxopn0yelv  8195  tz7.48lem  8412  dif20el  8472  oeordi  8554  oeeulem  8568  oeeui  8569  nnawordex  8604  swoer  8705  eceqoveq  8798  mapsnconst  8868  resixpfo  8912  boxcutc  8917  sdomnen  8955  en0  8992  en0ALT  8993  en0r  8994  en1  8998  dom0  9075  fodomr  9098  dif1enlem  9126  dif1enlemOLD  9127  unxpdomlem3  9206  fineqvlem  9216  infn0  9258  fodomfir  9286  f1opwfi  9314  fsuppcolem  9359  fsuppco  9360  mapfienlem1  9363  mapfienlem2  9364  supub  9417  suplub  9418  ordtypelem2  9479  ordtypelem3  9480  ordtypelem6  9483  ordtypelem7  9484  wemapso2lem  9512  wdom2d  9540  brwdom3  9542  ixpiunwdom  9550  inf3lem2  9589  inf3lem6  9593  oancom  9611  infdifsn  9617  cantnfp1lem3  9640  cantnflem3  9651  cantnflem4  9652  oef1o  9658  cnfcom3  9664  tctr  9700  frinsg  9711  tz9.12lem3  9749  scottex  9845  cardid2  9913  infxpenlem  9973  acni3  10007  cardaleph  10049  iscard3  10053  dfac5lem4  10086  dfac5lem5  10087  dfac5lem4OLD  10088  kmlem1  10111  cofsmo  10229  fin4en1  10269  enfin2i  10281  fin23lem28  10300  fin23lem38  10309  isf32lem6  10318  enfin1ai  10344  hsmexlem2  10387  hsmexlem4  10389  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  ac6num  10439  zorn2lem2  10457  brdom3  10488  alephval2  10532  alephreg  10542  pwcfsdom  10543  smobeth  10546  fpwwe2lem5  10595  fpwwe2lem12  10602  canthp1lem2  10613  pwfseqlem3  10620  hargch  10633  winalim2  10656  gchina  10659  inar1  10735  0npi  10842  mulclpi  10853  mulcanpi  10860  nlt1pi  10866  nqereu  10889  prcdnq  10953  prnmax  10955  ltresr2  11101  axrnegex  11122  axpre-sup  11129  eluz2gt1  12886  1nuz2  12890  zsupss  12903  rpgt0  12971  ixxss1  13331  ixxss2  13332  ixxss12  13333  lbioo  13344  ubioo  13345  iccss2  13385  iccssico2  13388  elfzuz3  13489  serge0  14028  expge0  14070  expge1  14071  expaddzlem  14077  hashrabsn1  14346  hashfun  14409  cshinj  14783  relexpuzrel  15025  shftfn  15046  01sqrexlem6  15220  rlimss  15475  lo1dm  15492  o1dm  15503  rlimrege0  15552  fsumf1o  15696  fsumge0  15768  incexc2  15811  supcvg  15829  fprodf1o  15919  divalglem9  16378  bitsfzolem  16411  bitsf1  16423  gcdcllem1  16476  bezout  16520  nprm  16665  dvdsprm  16680  coprm  16688  dfphi2  16751  phimullem  16756  phisum  16768  expnprm  16880  prmreclem2  16895  prmreclem5  16898  1arith  16905  4sqlem18  16940  vdwnnlem3  16975  ramtlecl  16978  rami  16993  0ram  16998  ramub1lem1  17004  prmgaplem5  17033  acsfiel  17622  isacs1i  17625  catlid  17651  catrid  17652  fullfo  17883  fthf1  17888  fthoppc  17894  invfuc  17946  prslem  18265  oduprs  18268  posi  18285  tleile  18387  dlatmjdi  18489  pslem  18538  tsrlin  18551  cnvtsr  18554  tsrdir  18570  mndid  18678  mhmf  18723  mhmlin  18727  mhm0  18728  mndind  18762  grpinvex  18882  grplinv  18928  mulgz  19041  mulgdirlem  19044  mulgdir  19045  mulgass  19050  nsgbi  19096  nmzbi  19103  ghmf  19159  ghmlin  19160  conjnsg  19193  gimf1o  19202  gagrpid  19233  gaf  19234  gaass  19236  psgnunilem5  19431  odid  19475  odf1o2  19510  gexid  19518  sylow1lem4  19538  pj1id  19636  efgredeu  19689  ablcmn  19724  cmncom  19735  mulgdi  19763  torsubg  19791  cyggenod2  19822  cygctb  19829  ghmcyg  19833  dprdf1o  19971  ablfacrplem  20004  ablfaclem2  20025  ablfac2  20028  simpg2nsg  20035  fincygsubgodexd  20052  crngmgp  20157  rnghmmgmhm  20359  rhmmhm  20395  rhmghm  20400  rimf1o  20410  nzrnz  20431  0ringbas  20444  subrgss  20488  subrg1cl  20496  rnghmsubcsetclem1  20547  zrinitorngc  20558  zrtermorngc  20559  rhmsubcsetclem1  20576  ringcinv  20587  zrtermoringc  20591  rrgeq0i  20615  domneq0  20624  domnrrg  20629  drngunit  20650  fldcrngd  20658  drngmgp  20661  drngid  20662  drngdomn  20665  issubdrg  20696  fldhmsubc  20701  fldsdrgfld  20714  cntzsdrg  20718  abvge0  20733  srngcnv  20763  lmhmlin  20949  lmimf1o  20977  lvecdrng  21019  lspsolvlem  21059  islbs3  21072  lbsextlem3  21077  2idlelbas  21181  2idlcpblrng  21188  zringunit  21383  prmirredlem  21389  irinitoringc  21396  znidomb  21478  cygzn  21487  psgndiflemB  21516  pjf  21629  frlmsslsp  21712  frlmlbs  21713  f1lindf  21738  assalem  21773  psrbaglefi  21842  psrbagleadd1  21844  mplelsfi  21911  mplsubrglem  21920  mplcoe1  21951  mplbas2  21956  opsrtoslem2  21970  mhpmulcl  22043  psdmul  22060  coe1mul2  22162  pmatcoe1fsupp  22595  toponuni  22808  tpsuni  22830  mretopd  22986  neips  23007  neiptoptop  23025  neiptopnei  23026  perflp  23048  perfi  23049  cnf  23140  cnpf  23141  cnpimaex  23150  cnima  23159  t0sep  23218  t1ficld  23221  hausnei  23222  pnrmcld  23236  cnrmi  23254  cmpcov  23283  tgcmp  23295  hauscmplem  23300  connclo  23309  1stcclb  23338  2ndcdisj  23350  llyi  23368  nllyi  23369  ptpjpre1  23465  ptpjcn  23505  ptpjopn  23506  ptclsg  23509  dfac14  23512  txdis1cn  23529  pthaus  23532  hauseqlcld  23540  txkgen  23546  xkococn  23554  txconn  23583  hmeocnvcn  23655  fbssfi  23731  filss  23747  uffixfr  23817  flimneiss  23860  flimelbas  23862  flimfnfcls  23922  alexsubb  23940  alexsubALT  23945  ptcmplem2  23947  ptcmplem3  23948  ptcmplem4  23949  tmdgsum2  23990  ghmcnp  24009  tgpt0  24013  qustgplem  24015  istdrg2  24072  vscacn  24080  tvctdrg  24087  uspreg  24168  ucncn  24179  neipcfilu  24190  cuspcvg  24195  psmetxrge0  24208  isxmet2d  24222  prdsxmetlem  24263  imasdsf1olem  24268  xmstopn  24346  mstopn  24347  stdbdxmet  24410  prdsxmslem2  24424  nrgabv  24556  nmvs  24571  nvclvec  24592  nmoge0  24616  nghmcl  24622  nmoi  24623  nghmghm  24629  nmhmlmhm  24644  nmhmnghm  24645  icccmp  24721  xrge0gsumle  24729  metds0  24746  metdstri  24747  metdsre  24749  metdseq0  24750  metdscnlem  24751  metnrmlem1a  24754  icopnfcnv  24847  xrhmeo  24851  pcoval1  24920  cvslvec  25032  cvsunit  25038  recvs  25053  cphreccllem  25085  cphsscph  25158  cmetcvg  25192  lmle  25208  cmscmet  25253  cmetcusp1  25260  hlcph  25271  minveclem4  25339  ivthlem3  25361  ovolmge0  25385  ovolicc1  25424  ovolicc2lem3  25427  ovolicc2lem5  25429  dyadmbl  25508  i1ff  25584  i1frn  25585  i1fima2  25587  itg2monolem1  25658  dvnres  25840  c1liplem1  25908  c1lip2  25910  dvge0  25918  lhop1lem  25925  itgsubstlem  25962  fta1glem2  26081  fta1b  26084  idomrootle  26085  plyf  26110  plypf1  26124  plyadd  26129  plymul  26130  coeeu  26137  dgrlem  26141  coeid  26150  elqaalem3  26236  aareccl  26241  eff1olem  26464  relogf1o  26482  logdmn0  26556  logcnlem2  26559  logcnlem3  26560  efopnlem1  26572  efopnlem2  26573  logtayl2  26578  cxpcn3lem  26664  cxpcn3  26665  logbgcd1irr  26711  atandmneg  26823  atandmcj  26826  efiatan2  26834  cosatan  26838  cosatanne0  26839  dvatan  26852  areage0  26880  cxp2lim  26894  jensenlem2  26905  jensen  26906  eldmgm  26939  dmgmaddn0  26940  dmlogdmgm  26941  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgambdd  26954  lgamucov  26955  ftalem3  26992  efnnfsumcl  27020  efchtdvds  27076  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  dvdsflf1o  27104  musum  27108  muinv  27110  mpodvdsmulf1o  27111  dvdsmulf1o  27113  lgsfle1  27224  lgsle1  27230  lgsdirprm  27249  lgsne0  27253  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  chebbnd1  27390  chtppilim  27393  chpchtlim  27397  chpo1ub  27398  dchrmusumlema  27411  dchrvmasumlem1  27413  dchrisum0lema  27432  dchrisum0lem2a  27435  logsqvma  27460  selberg3lem2  27476  pntrsumo1  27483  pnt2  27531  ostthlem1  27545  ostth3  27556  sltval2  27575  leftlt  27782  rightgt  27783  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  elons2  28166  onsleft  28168  sltonold  28169  onscutleft  28171  onscutlt  28172  axtgcgrrflx  28396  axtgcgrid  28397  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgcont1  28402  tglng  28480  axcontlem7  28904  axcontlem10  28907  upgrle  29024  umgredg2  29034  lfgredgge2  29058  usgredg2ALT  29127  usgr1vr  29189  usgrexmpledg  29196  upgrres1  29247  fusgrvtxfi  29253  vtxnbuvtx  29325  cusgrcplgr  29354  vdumgr0  29415  vtxdgoddnumeven  29488  trlres  29635  usgr2pth  29701  cyclispthon  29741  clwwlknlen  29968  clwwnonrepclwwnon  30281  2clwwlk2  30284  ablocom  30484  phpar2  30759  cbncms  30801  hlph  30825  hcaucvg  31122  hlimconvi  31127  shaddcl  31153  shmulcl  31154  chlimi  31170  chcompl  31178  choc1  31263  nmopre  31806  cnopc  31849  lnopl  31850  unop  31851  hmop  31858  cnfnc  31866  lnfnl  31867  nlelshi  31996  cnlnadjlem5  32007  elpjidm  32120  mdslle1i  32253  mdslle2i  32254  atcv0  32278  chpssati  32299  aciunf1lem  32593  padct  32650  ssnnssfz  32717  ccatf1  32877  swrdrndisj  32886  ressprs  32897  resspos  32899  resstos  32900  pwrssmgc  32933  ogrpinv0le  33036  ogrpsub  33037  ogrpaddlt  33038  wrdpmtrlast  33057  cyc3evpm  33114  cycpmgcl  33117  cycpmconjslem2  33119  cyc3conja  33121  isarchi3  33148  archirng  33149  archirngz  33150  archiabllem1a  33152  archiabllem1b  33153  archiabllem2a  33155  archiabllem2c  33156  archiabllem2b  33157  archiabl  33159  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrun  33207  isdrng4  33252  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  ofldtos  33296  ofldlt1  33298  ofldchr  33299  suborng  33300  subofld  33301  isarchiofld  33302  nn0omnd  33323  quslsm  33383  nsgmgclem  33389  nsgmgc  33390  prmidl0  33428  qsidomlem1  33430  mxidlirred  33450  krull  33457  ufdprmidl  33519  1arithufdlem4  33525  sradrng  33585  extdg1id  33668  ply1annnr  33700  madjusmdetlem4  33827  qtophaus  33833  crefi  33844  cmpcref  33847  cmppcmp  33855  pcmplfin  33857  zart0  33876  tpr2rico  33909  rge0scvg  33946  zrhunitpreima  33973  qqhrhm  33986  esummono  34051  gsumesum  34056  esumrnmpt2  34065  esumpinfval  34070  esumpcvgval  34075  esumpmono  34076  0elsiga  34111  sigaclcu  34114  issgon  34120  inelpisys  34151  ldsysgenld  34157  ldgenpisyslem1  34160  sxuni  34190  isrnmeas  34197  measvuni  34211  measssd  34212  ddemeas  34233  imambfm  34260  elmbfmvol2  34265  dya2icoseg2  34276  omssubaddlem  34297  omssubadd  34298  carsgsigalem  34313  pmeasmono  34322  sibfinima  34337  oddpwdc  34352  oddpwdcv  34353  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartlemr  34372  eulerpartlemgvv  34374  eulerpartlemgs2  34378  fiblem  34396  probtot  34410  ballotlem4  34497  ballotlem5  34498  ballotlemfrc  34525  ballotlemirc  34530  ballotth  34536  hgt750lemb  34654  bnj642  34745  bnj643  34746  bnj645  34747  bnj707  34752  bnj1379  34827  bnj1538  34852  bnj110  34855  bnj93  34860  bnj906  34927  bnj1006  34957  bnj1110  34979  bnj1121  34982  bnj1204  35009  bnj1321  35024  bnj1364  35025  bnj1398  35031  bnj1450  35047  bnj1312  35055  bnj1501  35064  bnj1523  35068  0nn0m1nnn0  35107  subfacp1lem3  35176  subfacp1lem5  35178  pconncn  35218  connpconn  35229  cvmcov  35257  cvmliftlem1  35279  cvmliftlem10  35288  cvmlift2lem11  35307  cvmlift2lem12  35308  msubff1  35550  mvhf1  35553  mthmpps  35576  mclspps  35578  fundmpss  35761  funpartfun  35938  fnetg  36340  neibastop1  36354  filnetlem3  36375  onint1  36444  weiunlem2  36458  weiunpo  36460  weiunse  36463  bj-nnfa  36723  bj-idres  37155  bj-rvecrr  37292  icorempo  37346  pibt2  37412  wl-nfeqfb  37531  phpreu  37605  fin2solem  37607  fin2so  37608  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  ptrest  37620  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  dvtan  37671  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  cover2  37716  indexa  37734  istotbnd3  37772  sstotbnd2  37775  sstotbnd  37776  totbndss  37778  equivtotbnd  37779  isbnd3  37785  totbndbnd  37790  equivbnd  37791  prdsbnd  37794  prdstotbnd  37795  heibor  37822  zrdivrng  37954  crngocom  38002  isfld2  38006  dmncrng  38057  eqvrelrel  38595  disjrel  38729  disjdmqscossss  38802  prter2  38881  toycom  38973  lsateln0  38995  lpssat  39013  lssat  39016  oposlem  39182  olop  39214  omllaw  39243  cvlexch1  39328  dihpN  41337  mapdordlem2  41638  linvh  42091  idomnnzpownz  42127  idomnnzgmulnz  42128  aks6d1c5lem2  42133  deg1pow  42136  redvmptabs  42355  readvrec2  42356  readvrec  42357  mhphflem  42591  prjspertr  42600  nacsfg  42700  nacsfix  42707  mzpindd  42741  diophrw  42754  diophrex  42770  rexzrexnn0  42799  pell1234qrdich  42856  rmspecnonsq  42902  rmspecfund  42904  rmspecpos  42912  monotoddzzfi  42938  ltrmxnn0  42945  rmxnn  42947  jm2.23  42992  jm3.1lem2  43014  dnnumch3  43043  lnmlssfg  43076  lnmlmic  43084  lnrlnm  43109  lnr2i  43112  lpirlnr  43113  hbtlem6  43125  hbt  43126  mnccoe  43134  proot1mul  43190  proot1hash  43191  deg1mhm  43196  ondif1i  43258  limnsuc  43261  cantnfresb  43320  succlg  43324  ntrneifv2  44076  grucollcld  44256  mnurndlem1  44277  ismnushort  44297  radcnvrat  44310  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  ordelordALT  44534  2uasbanh  44558  ordelordALTVD  44863  relprel  44948  elixpconstg  45090  rabidim2  45103  disjinfi  45193  supminfxr2  45472  sumnnodd  45635  stoweidlem7  46012  stoweidlem14  46019  stoweidlem16  46021  stoweidlem24  46029  stoweidlem31  46036  stoweidlem54  46059  wallispilem3  46072  fourierdlem42  46154  fourierdlem48  46159  fourierdlem51  46162  fourierdlem64  46175  fourierdlem76  46187  fourierdlem79  46190  fourierdlem81  46192  fourierdlem87  46198  etransclem28  46267  etransclem32  46271  sge0fodjrnlem  46421  hoidmvlelem3  46602  ovolval5lem3  46659  pimrecltpos  46713  pimrecltneg  46729  issmflem  46732  smfaddlem1  46768  smfsuplem1  46816  smfsuplem3  46818  smflimsuplem7  46831  smfliminflem  46835  tworepnotupword  46891  nfunsnafv  47147  faovcl  47205  tz6.12-2-afv2  47242  tz6.12i-afv2  47248  sprel  47489  evendiv2z  47637  oddp1div2z  47638  2dvdseven  47658  2ndvdsodd  47660  perfectALTVlem1  47726  sbgoldbm  47789  upgrimtrls  47910  upgrimpthslem1  47911  upgrimspths  47914  upgrimcycls  47915  uhgrimisgrgric  47935  gpgprismgr4cycllem2  48090  clintopcllaw  48203  uzlidlring  48227  rngccatidALTV  48264  funcringcsetcALTV2lem7  48288  ringccatidALTV  48298  ringcinvALTV  48302  funcringcsetclem7ALTV  48311  fldhmsubcALTV  48325  ssnn0ssfz  48341  el0ldepsnzr  48460  regt1loggt0  48529  elbigodm  48548  fllogbd  48553  rrx2xpref1o  48711  unilbss  48810  fdomne0  48842  f002  48846  xpco2  48849  imaf1homlem  49100  idemb  49152  uobeq2  49394  thincmo2  49419  thincmoALT  49422  fullthinc  49443  idfudiag1  49518  elsetrecslem  49692