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  1521  eumo  2579  reurmo  3354  pssne  4052  pssn2lp  4057  ssnpss  4059  eldifn  4085  elinel2  4155  rabsnt  4689  eldifsni  4747  unimax  4901  ssintub  4922  moop2  5451  pwssun  5517  weso  5616  opelxp2  5668  predpo  6282  frpoinsg  6302  ordwe  6331  funmo  6509  funopg  6527  funun  6539  fununi  6568  funimaexg  6580  fndm  6596  frn  6670  f1ss  6736  f1ssr  6737  forn  6750  f1f1orn  6786  f1orescnv  6790  f1imacnv  6791  funcocnv2  6800  dffv2  6930  exfo  7052  foelrn  7054  foelrnf  7055  isorel  7274  isoini2  7287  f1ofveu  7354  fovcld  7487  onminesb  7740  onminsb  7741  tfisg  7798  tfis  7799  limomss  7815  nnlim  7824  ssnlim  7830  resf1ext2b  7879  curry1  8048  curry2  8051  f1o2ndf1  8066  fnwelem  8075  mpoxopn0yelv  8157  tz7.48lem  8374  dif20el  8434  oeordi  8517  oeeulem  8531  oeeui  8532  nnawordex  8567  swoer  8669  eceqoveq  8763  mapsnconst  8834  resixpfo  8878  boxcutc  8883  sdomnen  8922  en0  8959  en0ALT  8960  en0r  8961  en1  8965  dom0  9037  fodomr  9060  dif1enlem  9088  unxpdomlem3  9162  fineqvlem  9170  infn0  9206  fodomfir  9232  f1opwfi  9260  fsuppcolem  9308  fsuppco  9309  mapfienlem1  9312  mapfienlem2  9313  supub  9366  suplub  9367  ordtypelem2  9428  ordtypelem3  9429  ordtypelem6  9432  ordtypelem7  9433  wemapso2lem  9461  wdom2d  9489  brwdom3  9491  ixpiunwdom  9499  inf3lem2  9542  inf3lem6  9546  oancom  9564  infdifsn  9570  cantnfp1lem3  9593  cantnflem3  9604  cantnflem4  9605  oef1o  9611  cnfcom3  9617  tctr  9651  frinsg  9667  tz9.12lem3  9705  scottex  9801  cardid2  9869  infxpenlem  9927  acni3  9961  cardaleph  10003  iscard3  10007  dfac5lem4  10040  dfac5lem5  10041  dfac5lem4OLD  10042  kmlem1  10065  cofsmo  10183  fin4en1  10223  enfin2i  10235  fin23lem28  10254  fin23lem38  10263  isf32lem6  10272  enfin1ai  10298  hsmexlem2  10341  hsmexlem4  10343  domtriomlem  10356  axdc2lem  10362  axdc3lem2  10365  ac6num  10393  zorn2lem2  10411  brdom3  10442  alephval2  10487  alephreg  10497  pwcfsdom  10498  smobeth  10501  fpwwe2lem5  10550  fpwwe2lem12  10557  canthp1lem2  10568  pwfseqlem3  10575  hargch  10588  winalim2  10611  gchina  10614  inar1  10690  0npi  10797  mulclpi  10808  mulcanpi  10815  nlt1pi  10821  nqereu  10844  prcdnq  10908  prnmax  10910  ltresr2  11056  axrnegex  11077  axpre-sup  11084  eluz2gt1  12837  1nuz2  12841  zsupss  12854  rpgt0  12922  ixxss1  13283  ixxss2  13284  ixxss12  13285  lbioo  13296  ubioo  13297  iccss2  13337  iccssico2  13340  elfzuz3  13441  serge0  13983  expge0  14025  expge1  14026  expaddzlem  14032  hashrabsn1  14301  hashfun  14364  cshinj  14738  relexpuzrel  14979  shftfn  15000  01sqrexlem6  15174  rlimss  15429  lo1dm  15446  o1dm  15457  rlimrege0  15506  fsumf1o  15650  fsumge0  15722  incexc2  15765  supcvg  15783  fprodf1o  15873  divalglem9  16332  bitsfzolem  16365  bitsf1  16377  gcdcllem1  16430  bezout  16474  nprm  16619  dvdsprm  16634  coprm  16642  dfphi2  16705  phimullem  16710  phisum  16722  expnprm  16834  prmreclem2  16849  prmreclem5  16852  1arith  16859  4sqlem18  16894  vdwnnlem3  16929  ramtlecl  16932  rami  16947  0ram  16952  ramub1lem1  16958  prmgaplem5  16987  acsfiel  17581  isacs1i  17584  catlid  17610  catrid  17611  fullfo  17842  fthf1  17847  fthoppc  17853  invfuc  17905  prslem  18224  oduprs  18227  posi  18244  tleile  18346  resspos  18356  resstos  18357  dlatmjdi  18450  pslem  18499  tsrlin  18512  cnvtsr  18515  tsrdir  18531  mndid  18673  mhmf  18718  mhmlin  18722  mhm0  18723  mndind  18757  grpinvex  18877  grplinv  18923  mulgz  19036  mulgdirlem  19039  mulgdir  19040  mulgass  19045  nsgbi  19090  nmzbi  19097  ghmf  19153  ghmlin  19154  conjnsg  19187  gimf1o  19196  gagrpid  19227  gaf  19228  gaass  19230  psgnunilem5  19427  odid  19471  odf1o2  19506  gexid  19514  sylow1lem4  19534  pj1id  19632  efgredeu  19685  ablcmn  19720  cmncom  19731  mulgdi  19759  torsubg  19787  cyggenod2  19818  cygctb  19825  ghmcyg  19829  dprdf1o  19967  ablfacrplem  20000  ablfaclem2  20021  ablfac2  20024  simpg2nsg  20031  fincygsubgodexd  20048  ogrpinv0le  20069  ogrpsub  20070  ogrpaddlt  20071  crngmgp  20180  rnghmmgmhm  20383  rhmmhm  20419  rhmghm  20423  rimf1o  20432  nzrnz  20452  0ringbas  20465  subrgss  20509  subrg1cl  20517  rnghmsubcsetclem1  20568  zrinitorngc  20579  zrtermorngc  20580  rhmsubcsetclem1  20597  ringcinv  20608  zrtermoringc  20612  rrgeq0i  20636  domneq0  20645  domnrrg  20650  drngunit  20671  fldcrngd  20679  drngmgp  20682  drngid  20683  drngdomn  20686  issubdrg  20717  fldhmsubc  20722  fldsdrgfld  20735  cntzsdrg  20739  abvge0  20754  srngcnv  20784  orngsqr  20803  ornglmulle  20804  orngrmulle  20805  ofldtos  20810  ofldlt1  20812  suborng  20813  subofld  20814  lmhmlin  20991  lmimf1o  21019  lvecdrng  21061  lspsolvlem  21101  islbs3  21114  lbsextlem3  21119  2idlelbas  21223  2idlcpblrng  21230  zringunit  21425  prmirredlem  21431  irinitoringc  21438  znidomb  21520  cygzn  21529  ofldchr  21535  psgndiflemB  21559  pjf  21672  frlmsslsp  21755  frlmlbs  21756  f1lindf  21781  assalem  21816  psrbaglefi  21886  psrbagleadd1  21888  mplelsfi  21954  mplsubrglem  21963  mplcoe1  21996  mplbas2  22001  opsrtoslem2  22015  mhpmulcl  22096  psdmul  22113  coe1mul2  22215  pmatcoe1fsupp  22649  toponuni  22862  tpsuni  22884  mretopd  23040  neips  23061  neiptoptop  23079  neiptopnei  23080  perflp  23102  perfi  23103  cnf  23194  cnpf  23195  cnpimaex  23204  cnima  23213  t0sep  23272  t1ficld  23275  hausnei  23276  pnrmcld  23290  cnrmi  23308  cmpcov  23337  tgcmp  23349  hauscmplem  23354  connclo  23363  1stcclb  23392  2ndcdisj  23404  llyi  23422  nllyi  23423  ptpjpre1  23519  ptpjcn  23559  ptpjopn  23560  ptclsg  23563  dfac14  23566  txdis1cn  23583  pthaus  23586  hauseqlcld  23594  txkgen  23600  xkococn  23608  txconn  23637  hmeocnvcn  23709  fbssfi  23785  filss  23801  uffixfr  23871  flimneiss  23914  flimelbas  23916  flimfnfcls  23976  alexsubb  23994  alexsubALT  23999  ptcmplem2  24001  ptcmplem3  24002  ptcmplem4  24003  tmdgsum2  24044  ghmcnp  24063  tgpt0  24067  qustgplem  24069  istdrg2  24126  vscacn  24134  tvctdrg  24141  uspreg  24221  ucncn  24232  neipcfilu  24243  cuspcvg  24248  psmetxrge0  24261  isxmet2d  24275  prdsxmetlem  24316  imasdsf1olem  24321  xmstopn  24399  mstopn  24400  stdbdxmet  24463  prdsxmslem2  24477  nrgabv  24609  nmvs  24624  nvclvec  24645  nmoge0  24669  nghmcl  24675  nmoi  24676  nghmghm  24682  nmhmlmhm  24697  nmhmnghm  24698  icccmp  24774  xrge0gsumle  24782  metds0  24799  metdstri  24800  metdsre  24802  metdseq0  24803  metdscnlem  24804  metnrmlem1a  24807  icopnfcnv  24900  xrhmeo  24904  pcoval1  24973  cvslvec  25085  cvsunit  25091  recvs  25106  cphreccllem  25138  cphsscph  25211  cmetcvg  25245  lmle  25261  cmscmet  25306  cmetcusp1  25313  hlcph  25324  minveclem4  25392  ivthlem3  25414  ovolmge0  25438  ovolicc1  25477  ovolicc2lem3  25480  ovolicc2lem5  25482  dyadmbl  25561  i1ff  25637  i1frn  25638  i1fima2  25640  itg2monolem1  25711  dvnres  25893  c1liplem1  25961  c1lip2  25963  dvge0  25971  lhop1lem  25978  itgsubstlem  26015  fta1glem2  26134  fta1b  26137  idomrootle  26138  plyf  26163  plypf1  26177  plyadd  26182  plymul  26183  coeeu  26190  dgrlem  26194  coeid  26203  elqaalem3  26289  aareccl  26294  eff1olem  26517  relogf1o  26535  logdmn0  26609  logcnlem2  26612  logcnlem3  26613  efopnlem1  26625  efopnlem2  26626  logtayl2  26631  cxpcn3lem  26717  cxpcn3  26718  logbgcd1irr  26764  atandmneg  26876  atandmcj  26879  efiatan2  26887  cosatan  26891  cosatanne0  26892  dvatan  26905  areage0  26933  cxp2lim  26947  jensenlem2  26958  jensen  26959  eldmgm  26992  dmgmaddn0  26993  dmlogdmgm  26994  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamgulmlem5  27003  lgambdd  27007  lgamucov  27008  ftalem3  27045  efnnfsumcl  27073  efchtdvds  27129  sqff1o  27152  fsumdvdsdiaglem  27153  dvdsppwf1o  27156  dvdsflf1o  27157  musum  27161  muinv  27163  mpodvdsmulf1o  27164  dvdsmulf1o  27166  lgsfle1  27277  lgsle1  27283  lgsdirprm  27302  lgsne0  27306  lgseisenlem3  27348  lgseisenlem4  27349  lgsquadlem1  27351  lgsquadlem2  27352  chebbnd1  27443  chtppilim  27446  chpchtlim  27450  chpo1ub  27451  dchrmusumlema  27464  dchrvmasumlem1  27466  dchrisum0lema  27485  dchrisum0lem2a  27488  logsqvma  27513  selberg3lem2  27529  pntrsumo1  27536  pnt2  27584  ostthlem1  27598  ostth3  27609  sltval2  27628  leftlt  27845  rightgt  27846  precsexlem8  28195  precsexlem9  28196  precsexlem11  28198  elons2  28239  onsleft  28241  sltonold  28242  onscutleft  28244  onscutlt  28245  zscut0  28387  axtgcgrrflx  28517  axtgcgrid  28518  axtgsegcon  28519  axtg5seg  28520  axtgbtwnid  28521  axtgpasch  28522  axtgcont1  28523  tglng  28601  axcontlem7  29026  axcontlem10  29029  upgrle  29146  umgredg2  29156  lfgredgge2  29180  usgredg2ALT  29249  usgr1vr  29311  usgrexmpledg  29318  upgrres1  29369  fusgrvtxfi  29375  vtxnbuvtx  29447  cusgrcplgr  29476  vdumgr0  29537  vtxdgoddnumeven  29610  trlres  29755  usgr2pth  29820  cyclispthon  29860  clwwlknlen  30090  clwwnonrepclwwnon  30403  2clwwlk2  30406  ablocom  30606  phpar2  30881  cbncms  30923  hlph  30947  hcaucvg  31244  hlimconvi  31249  shaddcl  31275  shmulcl  31276  chlimi  31292  chcompl  31300  choc1  31385  nmopre  31928  cnopc  31971  lnopl  31972  unop  31973  hmop  31980  cnfnc  31988  lnfnl  31989  nlelshi  32118  cnlnadjlem5  32129  elpjidm  32242  mdslle1i  32375  mdslle2i  32376  atcv0  32400  aciunf1lem  32722  padct  32778  ssnnssfz  32848  ccatf1  33012  swrdrndisj  33020  ressprs  33029  pwrssmgc  33063  wrdpmtrlast  33156  cyc3evpm  33213  cycpmgcl  33216  cycpmconjslem2  33218  cyc3conja  33220  isarchi3  33250  archirng  33251  archirngz  33252  archiabllem1a  33254  archiabllem1b  33255  archiabllem2a  33257  archiabllem2c  33258  archiabllem2b  33259  archiabl  33261  isarchiofld  33262  elrgspnlem1  33305  elrgspnlem2  33306  elrgspnlem4  33308  elrgspnsubrun  33312  isdrng4  33358  nn0omnd  33406  quslsm  33467  nsgmgclem  33473  nsgmgc  33474  prmidl0  33512  qsidomlem1  33514  mxidlirred  33534  krull  33541  ufdprmidl  33603  1arithufdlem4  33609  extvfvcl  33682  mplvrpmlem  33689  mplvrpmga  33691  sradrng  33719  extdg1id  33804  ply1annnr  33841  madjusmdetlem4  33968  qtophaus  33974  crefi  33985  cmpcref  33988  cmppcmp  33996  pcmplfin  33998  zart0  34017  tpr2rico  34050  rge0scvg  34087  zrhunitpreima  34114  qqhrhm  34127  esummono  34192  gsumesum  34197  esumrnmpt2  34206  esumpinfval  34211  esumpcvgval  34216  esumpmono  34217  0elsiga  34252  sigaclcu  34255  issgon  34261  inelpisys  34292  ldsysgenld  34298  ldgenpisyslem1  34301  sxuni  34331  isrnmeas  34338  measvuni  34352  measssd  34353  ddemeas  34374  imambfm  34400  elmbfmvol2  34405  dya2icoseg2  34416  omssubaddlem  34437  omssubadd  34438  carsgsigalem  34453  pmeasmono  34462  sibfinima  34477  oddpwdc  34492  oddpwdcv  34493  eulerpartlemf  34508  eulerpartlemt  34509  eulerpartlemr  34512  eulerpartlemgvv  34514  eulerpartlemgs2  34518  fiblem  34536  probtot  34550  ballotlem4  34637  ballotlem5  34638  ballotlemfrc  34665  ballotlemirc  34670  ballotth  34676  hgt750lemb  34794  bnj642  34885  bnj643  34886  bnj645  34887  bnj707  34892  bnj1379  34967  bnj1538  34992  bnj110  34995  bnj93  35000  bnj906  35067  bnj1006  35097  bnj1110  35119  bnj1121  35122  bnj1204  35149  bnj1321  35164  bnj1364  35165  bnj1398  35171  bnj1450  35187  bnj1312  35195  bnj1501  35204  bnj1523  35208  tz9.1regs  35271  0nn0m1nnn0  35288  subfacp1lem3  35357  subfacp1lem5  35359  pconncn  35399  connpconn  35410  cvmcov  35438  cvmliftlem1  35460  cvmliftlem10  35469  cvmlift2lem11  35488  cvmlift2lem12  35489  msubff1  35731  mvhf1  35734  mthmpps  35757  mclspps  35759  fundmpss  35942  funpartfun  36118  fnetg  36520  neibastop1  36534  filnetlem3  36555  onint1  36624  weiunlem2  36638  weiunpo  36640  weiunse  36643  bj-nnfa  36904  bj-idres  37336  bj-rvecrr  37473  icorempo  37527  pibt2  37593  wl-nfeqfb  37712  phpreu  37776  fin2solem  37778  fin2so  37779  lindsenlbs  37787  matunitlindflem1  37788  matunitlindflem2  37789  matunitlindf  37790  ptrest  37791  poimirlem1  37793  poimirlem2  37794  poimirlem3  37795  poimirlem4  37796  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem9  37801  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem13  37805  poimirlem14  37806  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem23  37815  poimirlem24  37816  poimirlem26  37818  poimirlem27  37819  poimirlem29  37821  poimirlem31  37823  mblfinlem2  37830  dvtan  37842  itg2gt0cn  37847  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  cover2  37887  indexa  37905  istotbnd3  37943  sstotbnd2  37946  sstotbnd  37947  totbndss  37949  equivtotbnd  37950  isbnd3  37956  totbndbnd  37961  equivbnd  37962  prdsbnd  37965  prdstotbnd  37966  heibor  37993  zrdivrng  38125  crngocom  38173  isfld2  38177  dmncrng  38228  eqvrelrel  38853  disjrel  39002  disjdmqscossss  39078  prter2  39178  toycom  39270  lsateln0  39292  lpssat  39310  lssat  39313  oposlem  39479  olop  39511  omllaw  39540  cvlexch1  39625  dihpN  41633  mapdordlem2  41934  linvh  42387  idomnnzpownz  42423  idomnnzgmulnz  42424  aks6d1c5lem2  42429  deg1pow  42432  redvmptabs  42651  readvrec2  42652  readvrec  42653  mhphflem  42875  prjspertr  42884  nacsfg  42983  nacsfix  42990  mzpindd  43024  diophrw  43037  diophrex  43053  rexzrexnn0  43082  pell1234qrdich  43139  rmspecnonsq  43185  rmspecfund  43187  rmspecpos  43194  monotoddzzfi  43220  ltrmxnn0  43227  rmxnn  43229  jm2.23  43274  jm3.1lem2  43296  dnnumch3  43325  lnmlssfg  43358  lnmlmic  43366  lnrlnm  43391  lnr2i  43394  lpirlnr  43395  hbtlem6  43407  hbt  43408  mnccoe  43416  proot1mul  43472  proot1hash  43473  deg1mhm  43478  ondif1i  43540  limnsuc  43543  cantnfresb  43602  succlg  43606  ntrneifv2  44357  grucollcld  44537  mnurndlem1  44558  ismnushort  44578  radcnvrat  44591  binomcxplemdvbinom  44630  binomcxplemcvg  44631  binomcxplemnotnn0  44633  ordelordALT  44814  2uasbanh  44838  ordelordALTVD  45143  relprel  45228  elixpconstg  45369  rabidim2  45382  disjinfi  45472  supminfxr2  45749  sumnnodd  45912  stoweidlem7  46287  stoweidlem14  46294  stoweidlem16  46296  stoweidlem24  46304  stoweidlem31  46311  stoweidlem54  46334  wallispilem3  46347  fourierdlem42  46429  fourierdlem48  46434  fourierdlem51  46437  fourierdlem64  46450  fourierdlem76  46462  fourierdlem79  46465  fourierdlem81  46467  fourierdlem87  46473  etransclem28  46542  etransclem32  46546  sge0fodjrnlem  46696  hoidmvlelem3  46877  ovolval5lem3  46934  pimrecltpos  46988  pimrecltneg  47004  issmflem  47007  smfaddlem1  47043  smfsuplem1  47091  smfsuplem3  47093  smflimsuplem7  47106  smfliminflem  47110  nfunsnafv  47424  faovcl  47482  tz6.12-2-afv2  47519  tz6.12i-afv2  47525  sprel  47766  evendiv2z  47914  oddp1div2z  47915  2dvdseven  47935  2ndvdsodd  47937  perfectALTVlem1  48003  sbgoldbm  48066  upgrimtrls  48188  upgrimpthslem1  48189  upgrimspths  48192  upgrimcycls  48193  uhgrimisgrgric  48213  gpgprismgr4cycllem2  48378  clintopcllaw  48493  uzlidlring  48517  rngccatidALTV  48554  funcringcsetcALTV2lem7  48578  ringccatidALTV  48588  ringcinvALTV  48592  funcringcsetclem7ALTV  48601  fldhmsubcALTV  48615  ssnn0ssfz  48631  el0ldepsnzr  48749  regt1loggt0  48818  elbigodm  48837  fllogbd  48842  rrx2xpref1o  49000  unilbss  49099  fdomne0  49131  f002  49135  xpco2  49138  imaf1homlem  49388  idemb  49440  uobeq2  49682  thincmo2  49707  thincmoALT  49710  fullthinc  49731  idfudiag1  49806  elsetrecslem  49980