Theorem simprbi 498

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simplbiim  509  xornan  1526  eumo  2582  reurmo  3348  pssne  4037  pssn2lp  4042  ssnpss  4044  eldifn  4069  elinel2  4138  rabsnt  4670  eldifsni  4730  unimax  4882  ssintub  4903  moop2  5450  pwssun  5517  weso  5616  opelxp2  5668  predpo  6281  frpoinsg  6301  ordwe  6330  funmo  6508  funopg  6526  funun  6538  fununi  6567  funimaexg  6579  fndm  6595  frn  6669  f1ss  6735  f1ssr  6736  forn  6749  f1f1orn  6785  f1orescnv  6789  f1imacnv  6790  funcocnv2  6799  dffv2  6929  exfo  7053  foelrn  7055  foelrnf  7056  isorel  7277  isoini2  7290  f1ofveu  7357  fovcld  7490  onminesb  7743  onminsb  7744  tfisg  7801  tfis  7802  limomss  7818  nnlim  7827  ssnlim  7833  resf1ext2b  7882  curry1  8050  curry2  8053  f1o2ndf1  8068  fnwelem  8078  mpoxopn0yelv  8160  tz7.48lem  8377  dif20el  8437  oeordi  8520  oeeulem  8534  oeeui  8535  nnawordex  8570  swoer  8672  eceqoveq  8766  mapsnconst  8837  resixpfo  8881  boxcutc  8886  sdomnen  8925  en0  8962  en0ALT  8963  en0r  8964  en1  8968  dom0  9040  fodomr  9063  dif1enlem  9091  unxpdomlem3  9165  fineqvlem  9173  infn0  9209  fodomfir  9235  f1opwfi  9263  fsuppcolem  9311  fsuppco  9312  mapfienlem1  9315  mapfienlem2  9316  supub  9369  suplub  9370  ordtypelem2  9431  ordtypelem3  9432  ordtypelem6  9435  ordtypelem7  9436  wemapso2lem  9464  wdom2d  9492  brwdom3  9494  ixpiunwdom  9502  inf3lem2  9548  inf3lem6  9552  oancom  9570  infdifsn  9576  cantnfp1lem3  9599  cantnflem3  9610  cantnflem4  9611  oef1o  9617  cnfcom3  9623  tctr  9657  frinsg  9673  tz9.12lem3  9711  scottex  9807  cardid2  9875  infxpenlem  9933  acni3  9967  cardaleph  10009  iscard3  10013  dfac5lem4  10046  dfac5lem5  10047  dfac5lem4OLD  10048  kmlem1  10071  cofsmo  10189  fin4en1  10229  enfin2i  10241  fin23lem28  10260  fin23lem38  10269  isf32lem6  10278  enfin1ai  10304  hsmexlem2  10347  hsmexlem4  10349  domtriomlem  10362  axdc2lem  10368  axdc3lem2  10371  ac6num  10399  zorn2lem2  10417  brdom3  10448  alephval2  10493  alephreg  10503  pwcfsdom  10504  smobeth  10507  fpwwe2lem5  10556  fpwwe2lem12  10563  canthp1lem2  10574  pwfseqlem3  10581  hargch  10594  winalim2  10617  gchina  10620  inar1  10696  0npi  10803  mulclpi  10814  mulcanpi  10821  nlt1pi  10827  nqereu  10850  prcdnq  10914  prnmax  10916  ltresr2  11062  axrnegex  11083  axpre-sup  11090  eluz2gt1  12868  1nuz2  12872  zsupss  12885  rpgt0  12953  ixxss1  13314  ixxss2  13315  ixxss12  13316  lbioo  13327  ubioo  13328  iccss2  13368  iccssico2  13371  elfzuz3  13473  serge0  14016  expge0  14058  expge1  14059  expaddzlem  14065  hashrabsn1  14334  hashfun  14397  cshinj  14771  relexpuzrel  15012  shftfn  15033  01sqrexlem6  15207  rlimss  15462  lo1dm  15479  o1dm  15490  rlimrege0  15539  fsumf1o  15683  fsumge0  15756  incexc2  15801  supcvg  15819  fprodf1o  15909  divalglem9  16368  bitsfzolem  16401  bitsf1  16413  gcdcllem1  16466  bezout  16510  nprm  16655  dvdsprm  16671  coprm  16679  dfphi2  16742  phimullem  16747  phisum  16759  expnprm  16871  prmreclem2  16886  prmreclem5  16889  1arith  16896  4sqlem18  16931  vdwnnlem3  16966  ramtlecl  16969  rami  16984  0ram  16989  ramub1lem1  16995  prmgaplem5  17024  acsfiel  17618  isacs1i  17621  catlid  17647  catrid  17648  fullfo  17879  fthf1  17884  fthoppc  17890  invfuc  17942  prslem  18261  oduprs  18264  posi  18281  tleile  18383  resspos  18393  resstos  18394  dlatmjdi  18487  pslem  18536  tsrlin  18549  cnvtsr  18552  tsrdir  18568  mndid  18710  mhmf  18755  mhmlin  18759  mhm0  18760  mndind  18794  grpinvex  18917  grplinv  18963  mulgz  19076  mulgdirlem  19079  mulgdir  19080  mulgass  19085  nsgbi  19130  nmzbi  19137  ghmf  19193  ghmlin  19194  conjnsg  19227  gimf1o  19236  gagrpid  19267  gaf  19268  gaass  19270  psgnunilem5  19467  odid  19511  odf1o2  19546  gexid  19554  sylow1lem4  19574  pj1id  19672  efgredeu  19725  ablcmn  19760  cmncom  19771  mulgdi  19799  torsubg  19827  cyggenod2  19858  cygctb  19865  ghmcyg  19869  dprdf1o  20007  ablfacrplem  20040  ablfaclem2  20061  ablfac2  20064  simpg2nsg  20071  fincygsubgodexd  20088  ogrpinv0le  20109  ogrpsub  20110  ogrpaddlt  20111  crngmgp  20220  rnghmmgmhm  20421  rhmmhm  20457  rhmghm  20461  rimf1o  20471  nzrnz  20494  0ringbas  20507  subrgss  20551  subrg1cl  20559  rnghmsubcsetclem1  20610  zrinitorngc  20621  zrtermorngc  20622  rhmsubcsetclem1  20639  ringcinv  20650  zrtermoringc  20654  rrgeq0i  20678  domneq0  20687  domnrrg  20692  drngunit  20713  fldcrngd  20721  drngmgp  20724  drngid  20725  drngdomn  20728  issubdrg  20759  fldhmsubc  20764  fldsdrgfld  20777  cntzsdrg  20781  abvge0  20796  srngcnv  20826  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  ofldtos  20852  ofldlt1  20854  suborng  20855  subofld  20856  lmhmlin  21032  lmimf1o  21060  lvecdrng  21102  lspsolvlem  21142  islbs3  21155  lbsextlem3  21160  2idlelbas  21264  2idlcpblrng  21271  zringunit  21448  prmirredlem  21454  irinitoringc  21461  znidomb  21543  cygzn  21552  ofldchr  21558  psgndiflemB  21582  pjf  21695  frlmsslsp  21778  frlmlbs  21779  f1lindf  21804  assalem  21839  psrbaglefi  21908  psrbagleadd1  21910  mplelsfi  21976  mplsubrglem  21985  mplcoe1  22020  mplbas2  22025  opsrtoslem2  22039  mhpmulcl  22144  psdmul  22161  coe1mul2  22262  pmatcoe1fsupp  22691  toponuni  22904  tpsuni  22926  mretopd  23082  neips  23103  neiptoptop  23121  neiptopnei  23122  perflp  23144  perfi  23145  cnf  23236  cnpf  23237  cnpimaex  23246  cnima  23255  t0sep  23314  t1ficld  23317  hausnei  23318  pnrmcld  23332  cnrmi  23350  cmpcov  23379  tgcmp  23391  hauscmplem  23396  connclo  23405  1stcclb  23434  2ndcdisj  23446  llyi  23464  nllyi  23465  ptpjpre1  23561  ptpjcn  23601  ptpjopn  23602  ptclsg  23605  dfac14  23608  txdis1cn  23625  pthaus  23628  hauseqlcld  23636  txkgen  23642  xkococn  23650  txconn  23679  hmeocnvcn  23751  fbssfi  23827  filss  23843  uffixfr  23913  flimneiss  23956  flimelbas  23958  flimfnfcls  24018  alexsubb  24036  alexsubALT  24041  ptcmplem2  24043  ptcmplem3  24044  ptcmplem4  24045  tmdgsum2  24086  ghmcnp  24105  tgpt0  24109  qustgplem  24111  istdrg2  24168  vscacn  24176  tvctdrg  24183  uspreg  24263  ucncn  24274  neipcfilu  24285  cuspcvg  24290  psmetxrge0  24303  isxmet2d  24317  prdsxmetlem  24358  imasdsf1olem  24363  xmstopn  24441  mstopn  24442  stdbdxmet  24505  prdsxmslem2  24519  nrgabv  24651  nmvs  24666  nvclvec  24687  nmoge0  24711  nghmcl  24717  nmoi  24718  nghmghm  24724  nmhmlmhm  24739  nmhmnghm  24740  icccmp  24816  xrge0gsumle  24824  metds0  24841  metdstri  24842  metdsre  24844  metdseq0  24845  metdscnlem  24846  metnrmlem1a  24849  icopnfcnv  24934  xrhmeo  24938  pcoval1  25005  cvslvec  25117  cvsunit  25123  recvs  25138  cphreccllem  25170  cphsscph  25243  cmetcvg  25277  lmle  25293  cmscmet  25338  cmetcusp1  25345  hlcph  25356  minveclem4  25424  ivthlem3  25445  ovolmge0  25469  ovolicc1  25508  ovolicc2lem3  25511  ovolicc2lem5  25513  dyadmbl  25592  i1ff  25668  i1frn  25669  i1fima2  25671  itg2monolem1  25742  dvnres  25923  c1liplem1  25988  c1lip2  25990  dvge0  25998  lhop1lem  26005  itgsubstlem  26040  fta1glem2  26159  fta1b  26162  idomrootle  26163  plyf  26188  plypf1  26202  plyadd  26207  plymul  26208  coeeu  26215  dgrlem  26219  coeid  26228  elqaalem3  26312  aareccl  26317  eff1olem  26537  relogf1o  26555  logdmn0  26629  logcnlem2  26632  logcnlem3  26633  efopnlem1  26645  efopnlem2  26646  logtayl2  26651  cxpcn3lem  26736  cxpcn3  26737  logbgcd1irr  26783  atandmneg  26895  atandmcj  26898  efiatan2  26906  cosatan  26910  cosatanne0  26911  dvatan  26924  areage0  26952  cxp2lim  26965  jensenlem2  26976  jensen  26977  eldmgm  27010  dmgmaddn0  27011  dmlogdmgm  27012  lgamgulmlem2  27018  lgamgulmlem3  27019  lgamgulmlem5  27021  lgambdd  27025  lgamucov  27026  ftalem3  27063  efnnfsumcl  27091  efchtdvds  27147  sqff1o  27170  fsumdvdsdiaglem  27171  dvdsppwf1o  27174  dvdsflf1o  27175  musum  27179  muinv  27181  mpodvdsmulf1o  27182  dvdsmulf1o  27184  lgsfle1  27294  lgsle1  27300  lgsdirprm  27319  lgsne0  27323  lgseisenlem3  27365  lgseisenlem4  27366  lgsquadlem1  27368  lgsquadlem2  27369  chebbnd1  27460  chtppilim  27463  chpchtlim  27467  chpo1ub  27468  dchrmusumlema  27481  dchrvmasumlem1  27483  dchrisum0lema  27502  dchrisum0lem2a  27505  logsqvma  27530  selberg3lem2  27546  pntrsumo1  27553  pnt2  27601  ostthlem1  27615  ostth3  27626  ltsval2  27645  leftlt  27870  rightgt  27871  precsexlem8  28231  precsexlem9  28232  precsexlem11  28234  elons2  28275  onleft  28277  ltonold  28278  oncutleft  28280  oncutlt  28281  zcuts0  28425  axtgcgrrflx  28555  axtgcgrid  28556  axtgsegcon  28557  axtg5seg  28558  axtgbtwnid  28559  axtgpasch  28560  axtgcont1  28561  tglng  28639  axcontlem7  29064  axcontlem10  29067  upgrle  29184  umgredg2  29194  lfgredgge2  29218  usgredg2ALT  29287  usgr1vr  29349  usgrexmpledg  29356  upgrres1  29407  fusgrvtxfi  29413  vtxnbuvtx  29485  cusgrcplgr  29514  vdumgr0  29574  vtxdgoddnumeven  29647  trlres  29792  usgr2pth  29857  cyclispthon  29897  clwwlknlen  30127  clwwnonrepclwwnon  30440  2clwwlk2  30443  ablocom  30644  phpar2  30919  cbncms  30961  hlph  30985  hcaucvg  31282  hlimconvi  31287  shaddcl  31313  shmulcl  31314  chlimi  31330  chcompl  31338  choc1  31423  nmopre  31966  cnopc  32009  lnopl  32010  unop  32011  hmop  32018  cnfnc  32026  lnfnl  32027  nlelshi  32156  cnlnadjlem5  32167  elpjidm  32280  mdslle1i  32413  mdslle2i  32414  atcv0  32438  aciunf1lem  32761  padct  32817  ssnnssfz  32886  ccatf1  33035  swrdrndisj  33043  ressprs  33052  pwrssmgc  33086  wrdpmtrlast  33181  cyc3evpm  33238  cycpmgcl  33241  cycpmconjslem2  33243  cyc3conja  33245  isarchi3  33275  archirng  33276  archirngz  33277  archiabllem1a  33279  archiabllem1b  33280  archiabllem2a  33282  archiabllem2c  33283  archiabllem2b  33284  archiabl  33286  isarchiofld  33287  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrun  33337  ricnzr1  33376  ricdomn1  33377  isdrng4  33386  nn0omnd  33434  quslsm  33495  nsgmgclem  33501  nsgmgc  33502  prmidl0  33540  qsidomlem1  33542  mxidlirred  33562  krull  33569  ufdprmidl  33631  1arithufdlem4  33637  extvfvcl  33727  mplvrpmlem  33734  mplvrpmga  33736  sradrng  33773  extdg1id  33857  ply1annnr  33894  madjusmdetlem4  34021  qtophaus  34027  crefi  34038  cmpcref  34041  cmppcmp  34049  pcmplfin  34051  zart0  34070  tpr2rico  34103  rge0scvg  34140  zrhunitpreima  34167  qqhrhm  34180  esummono  34245  gsumesum  34250  esumrnmpt2  34259  esumpinfval  34264  esumpcvgval  34269  esumpmono  34270  0elsiga  34305  sigaclcu  34308  issgon  34314  inelpisys  34345  ldsysgenld  34351  ldgenpisyslem1  34354  sxuni  34384  isrnmeas  34391  measvuni  34405  measssd  34406  ddemeas  34427  imambfm  34453  elmbfmvol2  34458  dya2icoseg2  34469  omssubaddlem  34490  omssubadd  34491  carsgsigalem  34506  pmeasmono  34515  sibfinima  34530  oddpwdc  34545  oddpwdcv  34546  eulerpartlemf  34561  eulerpartlemt  34562  eulerpartlemr  34565  eulerpartlemgvv  34567  eulerpartlemgs2  34571  fiblem  34589  probtot  34603  ballotlem4  34690  ballotlem5  34691  ballotlemfrc  34718  ballotlemirc  34723  ballotth  34729  hgt750lemb  34847  bnj642  34938  bnj643  34939  bnj645  34940  bnj707  34945  bnj1379  35019  bnj1538  35044  bnj110  35047  bnj93  35052  bnj906  35119  bnj1006  35149  bnj1110  35171  bnj1121  35174  bnj1204  35201  bnj1321  35216  bnj1364  35217  bnj1398  35223  bnj1450  35239  bnj1312  35247  bnj1501  35256  bnj1523  35260  tz9.1regs  35325  0nn0m1nnn0  35342  subfacp1lem3  35411  subfacp1lem5  35413  pconncn  35453  connpconn  35464  cvmcov  35492  cvmliftlem1  35514  cvmliftlem10  35523  cvmlift2lem11  35542  cvmlift2lem12  35543  msubff1  35785  mvhf1  35788  mthmpps  35811  mclspps  35813  fundmpss  35996  funpartfun  36172  fnetg  36574  neibastop1  36588  filnetlem3  36609  onint1  36678  weiunlem  36692  weiunpo  36694  weiunse  36697  bj-nnfa  37072  bj-idres  37521  bj-rvecrr  37658  icorempo  37714  pibt2  37780  wl-nfeqfb  37908  phpreu  37972  fin2solem  37974  fin2so  37975  lindsenlbs  37983  matunitlindflem1  37984  matunitlindflem2  37985  matunitlindf  37986  ptrest  37987  poimirlem1  37989  poimirlem2  37990  poimirlem3  37991  poimirlem4  37992  poimirlem5  37993  poimirlem6  37994  poimirlem7  37995  poimirlem8  37996  poimirlem9  37997  poimirlem10  37998  poimirlem11  37999  poimirlem12  38000  poimirlem13  38001  poimirlem14  38002  poimirlem15  38003  poimirlem16  38004  poimirlem17  38005  poimirlem18  38006  poimirlem19  38007  poimirlem20  38008  poimirlem21  38009  poimirlem22  38010  poimirlem23  38011  poimirlem24  38012  poimirlem26  38014  poimirlem27  38015  poimirlem29  38017  poimirlem31  38019  mblfinlem2  38026  dvtan  38038  itg2gt0cn  38043  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  cover2  38083  indexa  38101  istotbnd3  38139  sstotbnd2  38142  sstotbnd  38143  totbndss  38145  equivtotbnd  38146  isbnd3  38152  totbndbnd  38157  equivbnd  38158  prdsbnd  38161  prdstotbnd  38162  heibor  38189  zrdivrng  38321  crngocom  38369  isfld2  38373  dmncrng  38424  eqvrelrel  39049  disjrel  39198  disjdmqscossss  39274  prter2  39374  toycom  39466  lsateln0  39488  lpssat  39506  lssat  39509  oposlem  39675  olop  39707  omllaw  39736  cvlexch1  39821  dihpN  41829  mapdordlem2  42130  linvh  42582  idomnnzpownz  42618  idomnnzgmulnz  42619  aks6d1c5lem2  42624  deg1pow  42627  redvmptabs  42838  readvrec2  42839  readvrec  42840  mhphflem  43047  prjspertr  43056  nacsfg  43155  nacsfix  43162  mzpindd  43196  diophrw  43209  diophrex  43225  rexzrexnn0  43250  pell1234qrdich  43307  rmspecnonsq  43353  rmspecfund  43355  rmspecpos  43362  monotoddzzfi  43388  ltrmxnn0  43395  rmxnn  43397  jm2.23  43442  jm3.1lem2  43464  dnnumch3  43493  lnmlssfg  43526  lnmlmic  43534  lnrlnm  43559  lnr2i  43562  lpirlnr  43563  hbtlem6  43575  hbt  43576  mnccoe  43584  proot1mul  43640  proot1hash  43641  deg1mhm  43646  ondif1i  43708  limnsuc  43711  cantnfresb  43770  succlg  43774  ntrneifv2  44525  grucollcld  44705  mnurndlem1  44726  ismnushort  44746  radcnvrat  44759  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  ordelordALT  44982  2uasbanh  45006  ordelordALTVD  45311  relprel  45396  elixpconstg  45537  rabidim2  45550  disjinfi  45640  supminfxr2  45913  sumnnodd  46076  stoweidlem7  46451  stoweidlem14  46458  stoweidlem16  46460  stoweidlem24  46468  stoweidlem31  46475  stoweidlem54  46498  wallispilem3  46511  fourierdlem42  46593  fourierdlem48  46598  fourierdlem51  46601  fourierdlem64  46614  fourierdlem76  46626  fourierdlem79  46629  fourierdlem81  46631  fourierdlem87  46637  etransclem28  46706  etransclem32  46710  sge0fodjrnlem  46860  hoidmvlelem3  47041  ovolval5lem3  47098  pimrecltpos  47152  pimrecltneg  47168  issmflem  47171  smfaddlem1  47207  smfsuplem1  47255  smfsuplem3  47257  smflimsuplem7  47270  smfliminflem  47274  nfunsnafv  47606  faovcl  47664  tz6.12-2-afv2  47701  tz6.12i-afv2  47707  sprel  47960  evendiv2z  48124  oddp1div2z  48125  2dvdseven  48145  2ndvdsodd  48147  perfectALTVlem1  48213  sbgoldbm  48276  upgrimtrls  48398  upgrimpthslem1  48399  upgrimspths  48402  upgrimcycls  48403  uhgrimisgrgric  48423  gpgprismgr4cycllem2  48588  clintopcllaw  48703  uzlidlring  48727  rngccatidALTV  48764  funcringcsetcALTV2lem7  48788  ringccatidALTV  48798  ringcinvALTV  48802  funcringcsetclem7ALTV  48811  fldhmsubcALTV  48825  ssnn0ssfz  48841  el0ldepsnzr  48959  regt1loggt0  49028  elbigodm  49047  fllogbd  49052  rrx2xpref1o  49210  unilbss  49309  fdomne0  49341  f002  49345  xpco2  49348  imaf1homlem  49598  idemb  49650  uobeq2  49892  thincmo2  49917  thincmoALT  49920  fullthinc  49941  idfudiag1  50016  elsetrecslem  50190