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  1516  eumo  2581  reurmo  3391  pssne  4122  pssn2lp  4127  ssnpss  4129  eldifn  4155  elinel2  4225  rabsnt  4756  eldifsni  4815  unimax  4968  ssintub  4990  moop2  5521  pwssun  5590  weso  5691  opelxp2  5743  predpo  6355  frpoinsg  6375  wfisgOLD  6386  ordwe  6408  funmo  6593  funmoOLD  6594  funopg  6612  funun  6624  fununi  6653  funimaexg  6664  fndm  6682  frn  6754  f1ss  6822  f1ssr  6823  forn  6837  f1f1orn  6873  f1orescnv  6877  f1imacnv  6878  funcocnv2  6887  dffv2  7017  exfo  7139  foelrn  7141  foelrnf  7142  isorel  7362  isoini2  7375  f1ofveu  7442  fovcld  7577  onminesb  7829  onminsb  7830  tfisg  7891  tfis  7892  limomss  7908  nnlim  7917  ssnlim  7923  curry1  8145  curry2  8148  f1o2ndf1  8163  fnwelem  8172  mpoxopn0yelv  8254  wfrlem5OLD  8369  tz7.48lem  8497  dif20el  8561  oeordi  8643  oeeulem  8657  oeeui  8658  nnawordex  8693  swoer  8794  eceqoveq  8880  mapsnconst  8950  resixpfo  8994  boxcutc  8999  sdomnen  9041  en0  9078  en0OLD  9079  en0ALT  9080  en0r  9081  en1  9086  en1OLD  9087  dom0  9168  fodomr  9194  dif1enlem  9222  dif1enlemOLD  9223  unxpdomlem3  9315  fineqvlem  9325  infn0  9368  fodomfir  9396  f1opwfi  9426  fsuppcolem  9470  fsuppco  9471  mapfienlem1  9474  mapfienlem2  9475  supub  9528  suplub  9529  ordtypelem2  9588  ordtypelem3  9589  ordtypelem6  9592  ordtypelem7  9593  wemapso2lem  9621  wdom2d  9649  brwdom3  9651  ixpiunwdom  9659  inf3lem2  9698  inf3lem6  9702  oancom  9720  infdifsn  9726  cantnfp1lem3  9749  cantnflem3  9760  cantnflem4  9761  oef1o  9767  cnfcom3  9773  tctr  9809  frinsg  9820  tz9.12lem3  9858  scottex  9954  cardid2  10022  infxpenlem  10082  acni3  10116  cardaleph  10158  iscard3  10162  dfac5lem4  10195  dfac5lem5  10196  dfac5lem4OLD  10197  kmlem1  10220  cofsmo  10338  fin4en1  10378  enfin2i  10390  fin23lem28  10409  fin23lem38  10418  isf32lem6  10427  enfin1ai  10453  hsmexlem2  10496  hsmexlem4  10498  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  ac6num  10548  zorn2lem2  10566  brdom3  10597  alephval2  10641  alephreg  10651  pwcfsdom  10652  smobeth  10655  fpwwe2lem5  10704  fpwwe2lem12  10711  canthp1lem2  10722  pwfseqlem3  10729  hargch  10742  winalim2  10765  gchina  10768  inar1  10844  0npi  10951  mulclpi  10962  mulcanpi  10969  nlt1pi  10975  nqereu  10998  prcdnq  11062  prnmax  11064  ltresr2  11210  axrnegex  11231  axpre-sup  11238  eluz2gt1  12985  1nuz2  12989  zsupss  13002  rpgt0  13069  ixxss1  13425  ixxss2  13426  ixxss12  13427  lbioo  13438  ubioo  13439  iccss2  13478  iccssico2  13481  elfzuz3  13581  serge0  14107  expge0  14149  expge1  14150  expaddzlem  14156  hashrabsn1  14423  hashfun  14486  cshinj  14859  relexpuzrel  15101  shftfn  15122  01sqrexlem6  15296  rlimss  15548  lo1dm  15565  o1dm  15576  rlimrege0  15625  fsumf1o  15771  fsumge0  15843  incexc2  15886  supcvg  15904  fprodf1o  15994  divalglem9  16449  bitsfzolem  16480  bitsf1  16492  gcdcllem1  16545  bezout  16590  nprm  16735  dvdsprm  16750  coprm  16758  dfphi2  16821  phimullem  16826  phisum  16837  expnprm  16949  prmreclem2  16964  prmreclem5  16967  1arith  16974  4sqlem18  17009  vdwnnlem3  17044  ramtlecl  17047  rami  17062  0ram  17067  ramub1lem1  17073  prmgaplem5  17102  acsfiel  17712  isacs1i  17715  catlid  17741  catrid  17742  fullfo  17979  fthf1  17984  fthoppc  17990  invfuc  18044  prslem  18368  posi  18387  tleile  18491  dlatmjdi  18593  pslem  18642  tsrlin  18655  cnvtsr  18658  tsrdir  18674  mndid  18782  mhmf  18824  mhmlin  18828  mhm0  18829  mndind  18863  grpinvex  18983  grplinv  19029  mulgz  19142  mulgdirlem  19145  mulgdir  19146  mulgass  19151  nsgbi  19197  nmzbi  19204  ghmf  19260  ghmlin  19261  conjnsg  19294  gimf1o  19303  gagrpid  19334  gaf  19335  gaass  19337  psgnunilem5  19536  odid  19580  odf1o2  19615  gexid  19623  sylow1lem4  19643  pj1id  19741  efgredeu  19794  ablcmn  19829  cmncom  19840  mulgdi  19868  torsubg  19896  cyggenod2  19927  cygctb  19934  ghmcyg  19938  dprdf1o  20076  ablfacrplem  20109  ablfaclem2  20130  ablfac2  20133  simpg2nsg  20140  fincygsubgodexd  20157  crngmgp  20268  rnghmmgmhm  20469  rhmmhm  20505  rhmghm  20510  rimf1o  20520  nzrnz  20541  0ringbas  20554  subrgss  20600  subrg1cl  20608  rnghmsubcsetclem1  20653  zrinitorngc  20664  zrtermorngc  20665  rhmsubcsetclem1  20682  ringcinv  20693  zrtermoringc  20697  rrgeq0i  20721  domneq0  20730  domnrrg  20735  drngunit  20756  fldcrngd  20764  drngmgp  20767  drngid  20768  drngdomn  20771  fldidomOLD  20794  issubdrg  20803  fldhmsubc  20808  fldsdrgfld  20821  cntzsdrg  20825  abvge0  20840  srngcnv  20870  lmhmlin  21057  lmimf1o  21085  lvecdrng  21127  lspsolvlem  21167  islbs3  21180  lbsextlem3  21185  2idlelbas  21297  2idlcpblrng  21304  zringunit  21500  prmirredlem  21506  irinitoringc  21513  znidomb  21603  cygzn  21612  psgndiflemB  21641  pjf  21756  frlmsslsp  21839  frlmlbs  21840  f1lindf  21865  assalem  21900  psrbaglefi  21969  psrbagleadd1  21971  mplelsfi  22038  mplsubrglem  22047  mplcoe1  22078  mplbas2  22083  opsrtoslem2  22103  mhpmulcl  22176  psdmul  22193  coe1mul2  22293  pmatcoe1fsupp  22728  toponuni  22941  tpsuni  22963  mretopd  23121  neips  23142  neiptoptop  23160  neiptopnei  23161  perflp  23183  perfi  23184  cnf  23275  cnpf  23276  cnpimaex  23285  cnima  23294  t0sep  23353  t1ficld  23356  hausnei  23357  pnrmcld  23371  cnrmi  23389  cmpcov  23418  tgcmp  23430  hauscmplem  23435  connclo  23444  1stcclb  23473  2ndcdisj  23485  llyi  23503  nllyi  23504  ptpjpre1  23600  ptpjcn  23640  ptpjopn  23641  ptclsg  23644  dfac14  23647  txdis1cn  23664  pthaus  23667  hauseqlcld  23675  txkgen  23681  xkococn  23689  txconn  23718  hmeocnvcn  23790  fbssfi  23866  filss  23882  uffixfr  23952  flimneiss  23995  flimelbas  23997  flimfnfcls  24057  alexsubb  24075  alexsubALT  24080  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  tmdgsum2  24125  ghmcnp  24144  tgpt0  24148  qustgplem  24150  istdrg2  24207  vscacn  24215  tvctdrg  24222  uspreg  24304  ucncn  24315  neipcfilu  24326  cuspcvg  24331  psmetxrge0  24344  isxmet2d  24358  prdsxmetlem  24399  imasdsf1olem  24404  xmstopn  24482  mstopn  24483  stdbdxmet  24549  prdsxmslem2  24563  nrgabv  24703  nmvs  24718  nvclvec  24739  nmoge0  24763  nghmcl  24769  nmoi  24770  nghmghm  24776  nmhmlmhm  24791  nmhmnghm  24792  icccmp  24866  xrge0gsumle  24874  metds0  24891  metdstri  24892  metdsre  24894  metdseq0  24895  metdscnlem  24896  metnrmlem1a  24899  icopnfcnv  24992  xrhmeo  24996  pcoval1  25065  cvslvec  25177  cvsunit  25183  recvs  25198  cphreccllem  25231  cphsscph  25304  cmetcvg  25338  lmle  25354  cmscmet  25399  cmetcusp1  25406  hlcph  25417  minveclem4  25485  ivthlem3  25507  ovolmge0  25531  ovolicc1  25570  ovolicc2lem3  25573  ovolicc2lem5  25575  dyadmbl  25654  i1ff  25730  i1frn  25731  i1fima2  25733  itg2monolem1  25805  dvnres  25987  c1liplem1  26055  c1lip2  26057  dvge0  26065  lhop1lem  26072  itgsubstlem  26109  fta1glem2  26228  fta1b  26231  idomrootle  26232  plyf  26257  plypf1  26271  plyadd  26276  plymul  26277  coeeu  26284  dgrlem  26288  coeid  26297  elqaalem3  26381  aareccl  26386  eff1olem  26608  relogf1o  26626  logdmn0  26700  logcnlem2  26703  logcnlem3  26704  efopnlem1  26716  efopnlem2  26717  logtayl2  26722  cxpcn3lem  26808  cxpcn3  26809  logbgcd1irr  26855  atandmneg  26967  atandmcj  26970  efiatan2  26978  cosatan  26982  cosatanne0  26983  dvatan  26996  areage0  27024  cxp2lim  27038  jensenlem2  27049  jensen  27050  eldmgm  27083  dmgmaddn0  27084  dmlogdmgm  27085  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgambdd  27098  lgamucov  27099  ftalem3  27136  efnnfsumcl  27164  efchtdvds  27220  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsppwf1o  27247  dvdsflf1o  27248  musum  27252  muinv  27254  mpodvdsmulf1o  27255  dvdsmulf1o  27257  lgsfle1  27368  lgsle1  27374  lgsdirprm  27393  lgsne0  27397  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  chebbnd1  27534  chtppilim  27537  chpchtlim  27541  chpo1ub  27542  dchrmusumlema  27555  dchrvmasumlem1  27557  dchrisum0lema  27576  dchrisum0lem2a  27579  logsqvma  27604  selberg3lem2  27620  pntrsumo1  27627  pnt2  27675  ostthlem1  27689  ostth3  27700  sltval2  27719  addsproplem2  28021  sleadd1  28040  negsid  28091  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  elons2  28299  sltonold  28301  onscutleft  28303  axtgcgrrflx  28488  axtgcgrid  28489  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  tglng  28572  axcontlem7  29003  axcontlem10  29006  upgrle  29125  umgredg2  29135  lfgredgge2  29159  usgredg2ALT  29228  usgr1vr  29290  usgrexmpledg  29297  upgrres1  29348  fusgrvtxfi  29354  vtxnbuvtx  29426  cusgrcplgr  29455  vdumgr0  29516  vtxdgoddnumeven  29589  trlres  29736  usgr2pth  29800  cyclispthon  29837  clwwlknlen  30064  clwwnonrepclwwnon  30377  2clwwlk2  30380  ablocom  30580  phpar2  30855  cbncms  30897  hlph  30921  hcaucvg  31218  hlimconvi  31223  shaddcl  31249  shmulcl  31250  chlimi  31266  chcompl  31274  choc1  31359  nmopre  31902  cnopc  31945  lnopl  31946  unop  31947  hmop  31954  cnfnc  31962  lnfnl  31963  nlelshi  32092  cnlnadjlem5  32103  elpjidm  32216  mdslle1i  32349  mdslle2i  32350  atcv0  32374  chpssati  32395  aciunf1lem  32680  padct  32733  ssnnssfz  32792  ccatf1  32915  swrdrndisj  32924  ressprs  32936  oduprs  32937  resspos  32939  resstos  32940  pwrssmgc  32973  ogrpinv0le  33065  ogrpsub  33066  ogrpaddlt  33067  wrdpmtrlast  33086  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  isarchi3  33167  archirng  33168  archirngz  33169  archiabllem1a  33171  archiabllem1b  33172  archiabllem2a  33174  archiabllem2c  33175  archiabllem2b  33176  archiabl  33178  isdrng4  33264  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  ofldtos  33306  ofldlt1  33308  ofldchr  33309  suborng  33310  subofld  33311  isarchiofld  33312  nn0omnd  33338  quslsm  33398  nsgmgclem  33404  nsgmgc  33405  prmidl0  33443  qsidomlem1  33445  mxidlirred  33465  krull  33472  ufdprmidl  33534  1arithufdlem4  33540  sradrng  33598  extdg1id  33676  ply1annnr  33696  madjusmdetlem4  33776  qtophaus  33782  crefi  33793  cmpcref  33796  cmppcmp  33804  pcmplfin  33806  zart0  33825  tpr2rico  33858  rge0scvg  33895  zrhunitpreima  33924  qqhrhm  33935  esummono  34018  gsumesum  34023  esumrnmpt2  34032  esumpinfval  34037  esumpcvgval  34042  esumpmono  34043  0elsiga  34078  sigaclcu  34081  issgon  34087  inelpisys  34118  ldsysgenld  34124  ldgenpisyslem1  34127  sxuni  34157  isrnmeas  34164  measvuni  34178  measssd  34179  ddemeas  34200  imambfm  34227  elmbfmvol2  34232  dya2icoseg2  34243  omssubaddlem  34264  omssubadd  34265  carsgsigalem  34280  pmeasmono  34289  sibfinima  34304  oddpwdc  34319  oddpwdcv  34320  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemgvv  34341  eulerpartlemgs2  34345  fiblem  34363  probtot  34377  ballotlem4  34463  ballotlem5  34464  ballotlemfrc  34491  ballotlemirc  34496  ballotth  34502  hgt750lemb  34633  bnj642  34724  bnj643  34725  bnj645  34726  bnj707  34731  bnj1379  34806  bnj1538  34831  bnj110  34834  bnj93  34839  bnj906  34906  bnj1006  34936  bnj1110  34958  bnj1121  34961  bnj1204  34988  bnj1321  35003  bnj1364  35004  bnj1398  35010  bnj1450  35026  bnj1312  35034  bnj1501  35043  bnj1523  35047  0nn0m1nnn0  35080  subfacp1lem3  35150  subfacp1lem5  35152  pconncn  35192  connpconn  35203  cvmcov  35231  cvmliftlem1  35253  cvmliftlem10  35262  cvmlift2lem11  35281  cvmlift2lem12  35282  msubff1  35524  mvhf1  35527  mthmpps  35550  mclspps  35552  fundmpss  35730  funpartfun  35907  fnetg  36311  neibastop1  36325  filnetlem3  36346  onint1  36415  weiunlem2  36429  weiunpo  36431  weiunse  36434  bj-nnfa  36694  bj-idres  37126  bj-rvecrr  37263  icorempo  37317  pibt2  37383  wl-nfeqfb  37490  phpreu  37564  fin2solem  37566  fin2so  37567  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  ptrest  37579  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem31  37611  mblfinlem2  37618  dvtan  37630  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  cover2  37675  indexa  37693  istotbnd3  37731  sstotbnd2  37734  sstotbnd  37735  totbndss  37737  equivtotbnd  37738  isbnd3  37744  totbndbnd  37749  equivbnd  37750  prdsbnd  37753  prdstotbnd  37754  heibor  37781  zrdivrng  37913  crngocom  37961  isfld2  37965  dmncrng  38016  eqvrelrel  38553  disjrel  38686  disjdmqscossss  38759  prter2  38837  toycom  38929  lsateln0  38951  lpssat  38969  lssat  38972  oposlem  39138  olop  39170  omllaw  39199  cvlexch1  39284  dihpN  41293  mapdordlem2  41594  linvh  42053  idomnnzpownz  42089  idomnnzgmulnz  42090  aks6d1c5lem2  42095  deg1pow  42098  mhphflem  42551  prjspertr  42560  nacsfg  42661  nacsfix  42668  mzpindd  42702  diophrw  42715  diophrex  42731  rexzrexnn0  42760  pell1234qrdich  42817  rmspecnonsq  42863  rmspecfund  42865  rmspecpos  42873  monotoddzzfi  42899  ltrmxnn0  42906  rmxnn  42908  jm2.23  42953  jm3.1lem2  42975  dnnumch3  43004  lnmlssfg  43037  lnmlmic  43045  lnrlnm  43070  lnr2i  43073  lpirlnr  43074  hbtlem6  43086  hbt  43087  mnccoe  43095  proot1mul  43155  proot1hash  43156  deg1mhm  43161  ondif1i  43224  limnsuc  43227  cantnfresb  43286  succlg  43290  ntrneifv2  44042  grucollcld  44229  mnurndlem1  44250  ismnushort  44270  radcnvrat  44283  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  ordelordALT  44508  2uasbanh  44532  ordelordALTVD  44838  elixpconstg  44991  rabidim2  45004  disjinfi  45099  supminfxr2  45384  sumnnodd  45551  stoweidlem7  45928  stoweidlem14  45935  stoweidlem16  45937  stoweidlem24  45945  stoweidlem31  45952  stoweidlem54  45975  wallispilem3  45988  fourierdlem42  46070  fourierdlem48  46075  fourierdlem51  46078  fourierdlem64  46091  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem87  46114  etransclem28  46183  etransclem32  46187  sge0fodjrnlem  46337  hoidmvlelem3  46518  ovolval5lem3  46575  pimrecltpos  46629  pimrecltneg  46645  issmflem  46648  smfaddlem1  46684  smfsuplem1  46732  smfsuplem3  46734  smflimsuplem7  46747  smfliminflem  46751  tworepnotupword  46805  nfunsnafv  47057  faovcl  47115  tz6.12-2-afv2  47152  tz6.12i-afv2  47158  sprel  47358  evendiv2z  47506  oddp1div2z  47507  2dvdseven  47527  2ndvdsodd  47529  perfectALTVlem1  47595  sbgoldbm  47658  uhgrimisgrgric  47783  clintopcllaw  47934  uzlidlring  47958  rngccatidALTV  47995  funcringcsetcALTV2lem7  48019  ringccatidALTV  48029  ringcinvALTV  48033  funcringcsetclem7ALTV  48042  fldhmsubcALTV  48056  ssnn0ssfz  48074  el0ldepsnzr  48196  regt1loggt0  48270  elbigodm  48289  fllogbd  48294  rrx2xpref1o  48452  unilbss  48549  fdomne0  48563  f002  48567  thincmo2  48695  thincmoALT  48697  fullthinc  48713  elsetrecslem  48791