Theorem simprbi 502

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simplbiim  513  xornan  1542  just2-df  2090  eumo  2608  reurmo  3373  pssne  4055  pssn2lp  4061  ssnpss  4063  eldifn  4088  elinel2  4157  rabsnt  4693  eldifsni  4753  unimax  4906  ssintub  4927  moop2  5476  pwssun  5544  weso  5643  opelxp2  5695  predpo  6314  frpoinsg  6334  ordwe  6363  funmo  6541  funopg  6559  funun  6571  fununi  6600  funimaexg  6612  fndm  6628  frn  6703  f1ss  6771  f1ssr  6772  forn  6785  f1f1orn  6822  f1orescnv  6826  f1imacnv  6827  funcocnv2  6836  dffv2  6966  exfo  7090  foelrn  7092  foelrnf  7093  isorel  7314  isoini2  7327  f1ofveu  7394  fovcld  7527  onminesb  7780  onminsb  7781  tfisg  7838  tfis  7839  limomss  7855  nnlim  7864  ssnlim  7870  resf1ext2b  7920  curry1  8087  curry2  8090  f1o2ndf1  8105  fnwelem  8115  mpoxopn0yelv  8197  tz7.48lem  8416  dif20el  8478  oeordi  8561  oeeulem  8575  oeeui  8576  nnawordex  8611  swoer  8714  eceqoveq  8808  mapsnconst  8878  resixpfo  8922  boxcutc  8927  sdomnen  8966  en0  9003  en0ALT  9004  en0r  9005  en1  9009  dom0  9081  fodomr  9104  dif1enlem  9132  unxpdomlem3  9206  fineqvlem  9214  infn0  9250  fodomfir  9275  f1opwfi  9301  fsuppcolem  9349  fsuppco  9350  mapfienlem1  9353  mapfienlem2  9354  supub  9407  suplub  9408  ordtypelem2  9469  ordtypelem3  9470  ordtypelem6  9473  ordtypelem7  9474  wemapso2lem  9502  wdom2d  9530  brwdom3  9532  ixpiunwdom  9540  inf3lem2  9586  inf3lem6  9590  oancom  9608  infdifsn  9614  cantnfp1lem3  9637  cantnflem3  9648  cantnflem4  9649  oef1o  9655  cnfcom3  9661  tctr  9695  frinsg  9711  tz9.12lem3  9749  scottex  9847  cardid2  9927  infxpenlem  9985  acni3  10019  cardaleph  10061  iscard3  10065  dfac5lem4  10098  dfac5lem5  10099  kmlem1  10122  cofsmo  10241  fin4en1  10281  enfin2i  10293  fin23lem28  10312  fin23lem38  10321  isf32lem6  10330  enfin1ai  10356  hsmexlem2  10399  hsmexlem4  10401  domtriomlem  10414  axdc2lem  10420  axdc3lem2  10423  ac6num  10451  zorn2lem2  10469  brdom3  10500  alephval2  10545  alephreg  10555  pwcfsdom  10556  smobeth  10559  fpwwe2lem5  10608  fpwwe2lem12  10615  canthp1lem2  10626  pwfseqlem3  10633  hargch  10646  winalim2  10669  gchina  10672  inar1  10748  0npi  10855  mulclpi  10866  mulcanpi  10873  nlt1pi  10879  nqereu  10902  prcdnq  10966  prnmax  10968  ltresr2  11114  axrnegex  11135  axpre-sup  11142  eluz2gt1  12935  1nuz2  12939  zsupss  12952  rpgt0  13020  ixxss1  13381  ixxss2  13382  ixxss12  13383  lbioo  13394  ubioo  13395  iccss2  13435  iccssico2  13438  elfzuz3  13540  serge0  14083  expge0  14125  expge1  14126  expaddzlem  14132  hashrabsn1  14401  hashfun  14464  cshinj  14838  relexpuzrel  15079  shftfn  15100  01sqrexlem6  15288  rlimss  15543  lo1dm  15560  o1dm  15571  rlimrege0  15620  fsumf1o  15764  fsumge0  15837  incexc2  15882  supcvg  15900  fprodf1o  15990  divalglem9  16449  bitsfzolem  16482  bitsf1  16494  gcdcllem1  16547  bezout  16591  nprm  16736  dvdsprm  16752  coprm  16760  dfphi2  16823  phimullem  16828  phisum  16840  expnprm  16952  prmreclem2  16967  prmreclem5  16970  1arith  16977  4sqlem18  17012  vdwnnlem3  17047  ramtlecl  17050  rami  17065  0ram  17070  ramub1lem1  17076  prmgaplem5  17105  acsfiel  17700  isacs1i  17703  catlid  17729  catrid  17730  fullfo  17961  fthf1  17966  fthoppc  17972  invfuc  18024  prslem  18343  oduprs  18346  posi  18363  tleile  18465  resspos  18475  resstos  18476  dlatmjdi  18569  pslem  18618  tsrlin  18631  cnvtsr  18634  tsrdir  18650  mndid  18792  mhmf  18837  mhmlin  18841  mhm0  18842  mndind  18877  grpinvex  19000  grplinv  19046  mulgz  19159  mulgdirlem  19162  mulgdir  19163  mulgass  19168  nsgbi  19214  nmzbi  19221  ghmf  19281  ghmlin  19282  conjnsg  19315  gimf1o  19324  gagrpid  19355  gaf  19356  gaass  19358  psgnunilem5  19555  odid  19599  odf1o2  19634  gexid  19642  sylow1lem4  19662  pj1id  19760  efgredeu  19813  ablcmn  19848  cmncom  19859  mulgdi  19887  torsubg  19915  cyggenod2  19946  cygctb  19953  ghmcyg  19957  dprdf1o  20095  ablfacrplem  20128  ablfaclem2  20149  ablfac2  20152  simpg2nsg  20159  fincygsubgodexd  20176  ogrpinv0le  20197  ogrpsub  20198  ogrpaddlt  20199  crngmgp  20314  rnghmmgmhm  20516  rhmmhm  20552  rhmghm  20556  rimf1o  20566  nzrnz  20589  0ringbas  20603  subrgss  20648  subrg1cl  20656  rnghmsubcsetclem1  20707  zrinitorngc  20718  zrtermorngc  20719  rhmsubcsetclem1  20736  ringcinv  20747  zrtermoringc  20751  rrgeq0i  20775  domneq0  20784  domnrrg  20788  drngunit  20809  fldcrngd  20817  drngmgp  20820  drngid  20821  drngdomn  20824  issubdrg  20852  fldhmsubc  20857  fldsdrgfld  20870  cntzsdrg  20874  abvge0  20889  srngcnv  20919  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  ofldtos  20945  ofldlt1  20947  suborng  20948  subofld  20949  lmhmlin  21125  lmimf1o  21153  lvecdrng  21195  lspsolvlem  21235  islbs3  21248  lbsextlem3  21253  2idlelbas  21365  2idlcpblrng  21372  prmidl0  21438  qsidomlem1  21440  zringunit  21576  prmirredlem  21582  irinitoringc  21589  znidomb  21671  cygzn  21680  ofldchr  21686  psgndiflemB  21710  pjf  21823  frlmsslsp  21906  frlmlbs  21907  f1lindf  21932  assalem  21967  psrbaglefi  22036  psrbagleadd1  22038  mplelsfi  22104  mplsubrglem  22113  mplcoe1  22148  mplbas2  22153  opsrtoslem2  22167  mhpmulcl  22272  psdmul  22289  coe1mul2  22390  pmatcoe1fsupp  22819  toponuni  23032  tpsuni  23054  mretopd  23210  neips  23231  neiptoptop  23249  neiptopnei  23250  perflp  23272  perfi  23273  cnf  23364  cnpf  23365  cnpimaex  23374  cnima  23383  t0sep  23442  t1ficld  23445  hausnei  23446  pnrmcld  23460  cnrmi  23478  cmpcov  23507  tgcmp  23519  hauscmplem  23524  connclo  23533  1stcclb  23562  2ndcdisj  23574  llyi  23592  nllyi  23593  ptpjpre1  23689  ptpjcn  23729  ptpjopn  23730  ptclsg  23733  dfac14  23736  txdis1cn  23753  pthaus  23756  hauseqlcld  23764  txkgen  23770  xkococn  23778  txconn  23807  hmeocnvcn  23879  fbssfi  23955  filss  23971  uffixfr  24041  flimneiss  24084  flimelbas  24086  flimfnfcls  24146  alexsubb  24164  alexsubALT  24169  ptcmplem2  24171  ptcmplem3  24172  ptcmplem4  24173  tmdgsum2  24214  ghmcnp  24233  tgpt0  24237  qustgplem  24239  istdrg2  24296  vscacn  24304  tvctdrg  24311  uspreg  24391  ucncn  24402  neipcfilu  24413  cuspcvg  24418  psmetxrge0  24431  isxmet2d  24445  prdsxmetlem  24486  imasdsf1olem  24491  xmstopn  24569  mstopn  24570  stdbdxmet  24633  prdsxmslem2  24647  nrgabv  24779  nmvs  24794  nvclvec  24815  nmoge0  24839  nghmcl  24845  nmoi  24846  nghmghm  24852  nmhmlmhm  24867  nmhmnghm  24868  icccmp  24944  xrge0gsumle  24952  metds0  24969  metdstri  24970  metdsre  24972  metdseq0  24973  metdscnlem  24974  metnrmlem1a  24977  icopnfcnv  25062  xrhmeo  25066  pcoval1  25133  cvslvec  25245  cvsunit  25251  recvs  25266  cphreccllem  25298  cphsscph  25371  cmetcvg  25405  lmle  25421  cmscmet  25466  cmetcusp1  25473  hlcph  25484  minveclem4  25552  ivthlem3  25573  ovolmge0  25597  ovolicc1  25636  ovolicc2lem3  25639  ovolicc2lem5  25641  dyadmbl  25720  i1ff  25796  i1frn  25797  i1fima2  25799  itg2monolem1  25870  dvnres  26051  c1liplem1  26116  c1lip2  26118  dvge0  26126  lhop1lem  26133  itgsubstlem  26168  fta1glem2  26287  fta1b  26290  idomrootle  26291  plyf  26316  plypf1  26330  plyadd  26335  plymul  26336  coeeu  26343  dgrlem  26347  coeid  26356  elqaalem3  26443  aareccl  26448  eff1olem  26671  relogf1o  26689  logdmn0  26763  logcnlem2  26766  logcnlem3  26767  efopnlem1  26779  efopnlem2  26780  logtayl2  26785  cxpcn3lem  26870  cxpcn3  26871  logbgcd1irr  26917  atandmneg  27029  atandmcj  27032  efiatan2  27040  cosatan  27044  cosatanne0  27045  dvatan  27058  areage0  27086  cxp2lim  27099  jensenlem2  27110  jensen  27111  eldmgm  27144  dmgmaddn0  27145  dmlogdmgm  27146  lgamgulmlem2  27152  lgamgulmlem3  27153  lgamgulmlem5  27155  lgambdd  27159  lgamucov  27160  ftalem3  27197  efnnfsumcl  27225  efchtdvds  27281  sqff1o  27304  fsumdvdsdiaglem  27305  dvdsppwf1o  27308  dvdsflf1o  27309  musum  27313  muinv  27315  mpodvdsmulf1o  27316  dvdsmulf1o  27318  lgsfle1  27428  lgsle1  27434  lgsdirprm  27453  lgsne0  27457  lgseisenlem3  27499  lgseisenlem4  27500  lgsquadlem1  27502  lgsquadlem2  27503  chebbnd1  27594  chtppilim  27597  chpchtlim  27601  chpo1ub  27602  dchrmusumlema  27615  dchrvmasumlem1  27617  dchrisum0lema  27636  dchrisum0lem2a  27639  logsqvma  27664  selberg3lem2  27680  pntrsumo1  27687  pnt2  27735  ostthlem1  27749  ostth3  27760  ltsval2  27778  leftlt  28004  rightgt  28005  precsexlem8  28365  precsexlem9  28366  precsexlem11  28368  elons2  28409  onleft  28411  ltonold  28412  oncutleft  28414  oncutlt  28415  zcuts0  28559  axtgcgrrflx  28689  axtgcgrid  28690  axtgsegcon  28691  axtg5seg  28692  axtgbtwnid  28693  axtgpasch  28694  axtgcont1  28695  tglng  28773  axcontlem7  29229  axcontlem10  29232  upgrle  29349  umgredg2  29359  lfgredgge2  29383  usgredg2ALT  29452  usgr1vr  29514  usgrexmpledg  29521  upgrres1  29572  fusgrvtxfi  29578  vtxnbuvtx  29650  cusgrcplgr  29679  vdumgr0  29739  vtxdgoddnumeven  29812  trlres  29957  usgr2pth  30022  cyclispthon  30062  clwwlknlen  30292  clwwnonrepclwwnon  30605  2clwwlk2  30608  ablocom  30809  phpar2  31084  cbncms  31126  hlph  31150  hcaucvg  31447  hlimconvi  31452  shaddcl  31478  shmulcl  31479  chlimi  31495  chcompl  31503  choc1  31588  nmopre  32131  cnopc  32174  lnopl  32175  unop  32176  hmop  32183  cnfnc  32191  lnfnl  32192  nlelshi  32321  cnlnadjlem5  32332  elpjidm  32445  mdslle1i  32578  mdslle2i  32579  atcv0  32603  aciunf1lem  32919  padct  32975  ssnnssfz  33044  ccatf1  33182  swrdrndisj  33190  ressprs  33199  pwrssmgc  33233  wrdpmtrlast  33326  cyc3evpm  33383  cycpmgcl  33386  cycpmconjslem2  33388  cyc3conja  33390  isarchi3  33420  archirng  33421  archirngz  33422  archiabllem1a  33424  archiabllem1b  33425  archiabllem2a  33427  archiabllem2c  33428  archiabllem2b  33429  archiabl  33431  isarchiofld  33432  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem4  33478  elrgspnsubrun  33482  ricnzr1  33521  ricdomn1  33522  isdrng4  33531  nn0omnd  33579  quslsm  33630  nsgmgclem  33636  nsgmgc  33637  mxidlirred  33672  krull  33678  ufdprmidl  33748  1arithufdlem4  33754  extvfvcl  33843  mplvrpmlem  33850  mplvrpmga  33852  sradrng  33889  extdg1id  33973  ply1annnr  34010  madjusmdetlem4  34137  qtophaus  34143  crefi  34154  cmpcref  34157  cmppcmp  34165  pcmplfin  34167  zart0  34186  tpr2rico  34219  rge0scvg  34256  zrhunitpreima  34283  qqhrhm  34296  esummono  34361  gsumesum  34366  esumrnmpt2  34375  esumpinfval  34380  esumpcvgval  34385  esumpmono  34386  0elsiga  34421  sigaclcu  34424  issgon  34430  inelpisys  34461  ldsysgenld  34467  ldgenpisyslem1  34470  sxuni  34500  isrnmeas  34507  measvuni  34521  measssd  34522  ddemeas  34543  imambfm  34569  elmbfmvol2  34574  dya2icoseg2  34585  omssubaddlem  34606  omssubadd  34607  carsgsigalem  34622  pmeasmono  34631  sibfinima  34646  oddpwdc  34661  oddpwdcv  34662  eulerpartlemf  34677  eulerpartlemt  34678  eulerpartlemr  34681  eulerpartlemgvv  34683  eulerpartlemgs2  34687  fiblem  34705  probtot  34719  ballotlem4  34806  ballotlem5  34807  ballotlemfrc  34834  ballotlemirc  34839  ballotth  34845  hgt750lemb  34960  bnj642  35054  bnj643  35055  bnj645  35056  bnj707  35061  bnj1379  35135  bnj1538  35160  bnj110  35163  bnj93  35168  bnj906  35235  bnj1006  35265  bnj1110  35287  bnj1121  35290  bnj1204  35317  bnj1321  35332  bnj1364  35333  bnj1398  35339  bnj1450  35355  bnj1312  35363  bnj1501  35372  bnj1523  35376  tz9.1regs  35442  onvfowev  35471  0nn0m1nnn0  35475  subfacp1lem3  35545  subfacp1lem5  35547  pconncn  35587  connpconn  35598  cvmcov  35626  cvmliftlem1  35648  cvmliftlem10  35657  cvmlift2lem11  35676  cvmlift2lem12  35677  msubff1  35919  mvhf1  35922  mthmpps  35945  mclspps  35947  fundmpss  36130  funpartfun  36306  fnetg  36718  neibastop1  36732  filnetlem3  36753  onint1  36822  weiunlem  36836  weiunpo  36838  weiunse  36841  bj-nnfa  37215  bj-idres  37664  bj-rvecrr  37801  icorempo  37857  pibt2  37923  wl-nfeqfb  38051  phpreu  38115  fin2solem  38117  fin2so  38118  lindsenlbs  38126  matunitlindflem1  38127  matunitlindflem2  38128  matunitlindf  38129  ptrest  38130  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  poimirlem29  38160  poimirlem31  38162  mblfinlem2  38169  dvtan  38181  itg2gt0cn  38186  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  cover2  38226  indexa  38244  istotbnd3  38282  sstotbnd2  38285  sstotbnd  38286  totbndss  38288  equivtotbnd  38289  isbnd3  38295  totbndbnd  38300  equivbnd  38301  prdsbnd  38304  prdstotbnd  38305  heibor  38332  zrdivrng  38464  crngocom  38512  isfld2  38516  dmncrng  38567  eqvrelrel  39192  disjrel  39341  disjdmqscossss  39417  prter2  39517  toycom  39609  lsateln0  39631  lpssat  39649  lssat  39652  oposlem  39818  olop  39850  omllaw  39879  cvlexch1  39964  dihpN  41972  mapdordlem2  42273  linvh  42725  idomnnzpownz  42761  idomnnzgmulnz  42762  aks6d1c5lem2  42767  deg1pow  42770  redvmptabs  42981  readvrec2  42982  readvrec  42983  mhphflem  43190  prjspertr  43199  nacsfg  43298  nacsfix  43305  mzpindd  43339  diophrw  43352  diophrex  43368  rexzrexnn0  43393  pell1234qrdich  43450  rmspecnonsq  43496  rmspecfund  43498  rmspecpos  43505  monotoddzzfi  43531  ltrmxnn0  43538  rmxnn  43540  jm2.23  43585  jm3.1lem2  43607  dnnumch3  43636  lnmlssfg  43669  lnmlmic  43677  lnrlnm  43702  lnr2i  43705  lpirlnr  43706  hbtlem6  43718  hbt  43719  mnccoe  43727  proot1mul  43783  proot1hash  43784  deg1mhm  43789  ondif1i  43851  limnsuc  43854  cantnfresb  43913  succlg  43917  ntrneifv2  44668  grucollcld  44834  mnurndlem1  44855  ismnushort  44875  radcnvrat  44888  binomcxplemdvbinom  44927  binomcxplemcvg  44928  binomcxplemnotnn0  44930  ordelordALT  45111  2uasbanh  45135  ordelordALTVD  45440  relprel  45525  elixpconstg  45665  rabidim2  45678  disjinfi  45768  supminfxr2  46041  sumnnodd  46204  stoweidlem7  46579  stoweidlem14  46586  stoweidlem16  46588  stoweidlem24  46596  stoweidlem31  46603  stoweidlem54  46626  wallispilem3  46639  fourierdlem42  46721  fourierdlem48  46726  fourierdlem51  46729  fourierdlem64  46742  fourierdlem76  46754  fourierdlem79  46757  fourierdlem81  46759  fourierdlem87  46765  etransclem28  46834  etransclem32  46838  sge0fodjrnlem  46988  hoidmvlelem3  47169  ovolval5lem3  47226  pimrecltpos  47280  pimrecltneg  47296  issmflem  47299  smfaddlem1  47335  smfsuplem1  47383  smfsuplem3  47385  smflimsuplem7  47398  smfliminflem  47402  nfunsnafv  47734  faovcl  47792  tz6.12-2-afv2  47829  tz6.12i-afv2  47835  sprel  48088  evendiv2z  48252  oddp1div2z  48253  2dvdseven  48273  2ndvdsodd  48275  perfectALTVlem1  48341  sbgoldbm  48404  upgrimtrls  48526  upgrimpthslem1  48527  upgrimspths  48530  upgrimcycls  48531  uhgrimisgrgric  48551  gpgprismgr4cycllem2  48716  clintopcllaw  48831  uzlidlring  48855  rngccatidALTV  48892  funcringcsetcALTV2lem7  48916  ringccatidALTV  48926  ringcinvALTV  48930  funcringcsetclem7ALTV  48939  fldhmsubcALTV  48953  ssnn0ssfz  48980  el0ldepsnzr  49098  regt1loggt0  49167  elbigodm  49186  fllogbd  49191  rrx2xpref1o  49349  unilbss  49447  fdomne0  49479  f002  49483  xpco2  49486  imaf1homlem  49736  idemb  49788  uobeq2  50030  thincmo2  50055  thincmoALT  50058  fullthinc  50079  idfudiag1  50154  elsetrecslem  50328