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  2571  reurmo  3357  pssne  4062  pssn2lp  4067  ssnpss  4069  eldifn  4095  elinel2  4165  rabsnt  4695  eldifsni  4754  unimax  4908  ssintub  4930  moop2  5462  pwssun  5530  weso  5629  opelxp2  5681  predpo  6296  frpoinsg  6316  ordwe  6345  funmo  6531  funmoOLD  6532  funopg  6550  funun  6562  fununi  6591  funimaexg  6603  fndm  6621  frn  6695  f1ss  6761  f1ssr  6762  forn  6775  f1f1orn  6811  f1orescnv  6815  f1imacnv  6816  funcocnv2  6825  dffv2  6956  exfo  7077  foelrn  7079  foelrnf  7080  isorel  7301  isoini2  7314  f1ofveu  7381  fovcld  7516  onminesb  7769  onminsb  7770  tfisg  7830  tfis  7831  limomss  7847  nnlim  7856  ssnlim  7862  resf1ext2b  7911  curry1  8083  curry2  8086  f1o2ndf1  8101  fnwelem  8110  mpoxopn0yelv  8192  tz7.48lem  8409  dif20el  8469  oeordi  8551  oeeulem  8565  oeeui  8566  nnawordex  8601  swoer  8702  eceqoveq  8795  mapsnconst  8865  resixpfo  8909  boxcutc  8914  sdomnen  8952  en0  8989  en0ALT  8990  en0r  8991  en1  8995  dom0  9069  fodomr  9092  dif1enlem  9120  dif1enlemOLD  9121  unxpdomlem3  9199  fineqvlem  9209  infn0  9251  fodomfir  9279  f1opwfi  9307  fsuppcolem  9352  fsuppco  9353  mapfienlem1  9356  mapfienlem2  9357  supub  9410  suplub  9411  ordtypelem2  9472  ordtypelem3  9473  ordtypelem6  9476  ordtypelem7  9477  wemapso2lem  9505  wdom2d  9533  brwdom3  9535  ixpiunwdom  9543  inf3lem2  9582  inf3lem6  9586  oancom  9604  infdifsn  9610  cantnfp1lem3  9633  cantnflem3  9644  cantnflem4  9645  oef1o  9651  cnfcom3  9657  tctr  9693  frinsg  9704  tz9.12lem3  9742  scottex  9838  cardid2  9906  infxpenlem  9966  acni3  10000  cardaleph  10042  iscard3  10046  dfac5lem4  10079  dfac5lem5  10080  dfac5lem4OLD  10081  kmlem1  10104  cofsmo  10222  fin4en1  10262  enfin2i  10274  fin23lem28  10293  fin23lem38  10302  isf32lem6  10311  enfin1ai  10337  hsmexlem2  10380  hsmexlem4  10382  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  ac6num  10432  zorn2lem2  10450  brdom3  10481  alephval2  10525  alephreg  10535  pwcfsdom  10536  smobeth  10539  fpwwe2lem5  10588  fpwwe2lem12  10595  canthp1lem2  10606  pwfseqlem3  10613  hargch  10626  winalim2  10649  gchina  10652  inar1  10728  0npi  10835  mulclpi  10846  mulcanpi  10853  nlt1pi  10859  nqereu  10882  prcdnq  10946  prnmax  10948  ltresr2  11094  axrnegex  11115  axpre-sup  11122  eluz2gt1  12879  1nuz2  12883  zsupss  12896  rpgt0  12964  ixxss1  13324  ixxss2  13325  ixxss12  13326  lbioo  13337  ubioo  13338  iccss2  13378  iccssico2  13381  elfzuz3  13482  serge0  14021  expge0  14063  expge1  14064  expaddzlem  14070  hashrabsn1  14339  hashfun  14402  cshinj  14776  relexpuzrel  15018  shftfn  15039  01sqrexlem6  15213  rlimss  15468  lo1dm  15485  o1dm  15496  rlimrege0  15545  fsumf1o  15689  fsumge0  15761  incexc2  15804  supcvg  15822  fprodf1o  15912  divalglem9  16371  bitsfzolem  16404  bitsf1  16416  gcdcllem1  16469  bezout  16513  nprm  16658  dvdsprm  16673  coprm  16681  dfphi2  16744  phimullem  16749  phisum  16761  expnprm  16873  prmreclem2  16888  prmreclem5  16891  1arith  16898  4sqlem18  16933  vdwnnlem3  16968  ramtlecl  16971  rami  16986  0ram  16991  ramub1lem1  16997  prmgaplem5  17026  acsfiel  17615  isacs1i  17618  catlid  17644  catrid  17645  fullfo  17876  fthf1  17881  fthoppc  17887  invfuc  17939  prslem  18258  oduprs  18261  posi  18278  tleile  18380  dlatmjdi  18482  pslem  18531  tsrlin  18544  cnvtsr  18547  tsrdir  18563  mndid  18671  mhmf  18716  mhmlin  18720  mhm0  18721  mndind  18755  grpinvex  18875  grplinv  18921  mulgz  19034  mulgdirlem  19037  mulgdir  19038  mulgass  19043  nsgbi  19089  nmzbi  19096  ghmf  19152  ghmlin  19153  conjnsg  19186  gimf1o  19195  gagrpid  19226  gaf  19227  gaass  19229  psgnunilem5  19424  odid  19468  odf1o2  19503  gexid  19511  sylow1lem4  19531  pj1id  19629  efgredeu  19682  ablcmn  19717  cmncom  19728  mulgdi  19756  torsubg  19784  cyggenod2  19815  cygctb  19822  ghmcyg  19826  dprdf1o  19964  ablfacrplem  19997  ablfaclem2  20018  ablfac2  20021  simpg2nsg  20028  fincygsubgodexd  20045  crngmgp  20150  rnghmmgmhm  20352  rhmmhm  20388  rhmghm  20393  rimf1o  20403  nzrnz  20424  0ringbas  20437  subrgss  20481  subrg1cl  20489  rnghmsubcsetclem1  20540  zrinitorngc  20551  zrtermorngc  20552  rhmsubcsetclem1  20569  ringcinv  20580  zrtermoringc  20584  rrgeq0i  20608  domneq0  20617  domnrrg  20622  drngunit  20643  fldcrngd  20651  drngmgp  20654  drngid  20655  drngdomn  20658  issubdrg  20689  fldhmsubc  20694  fldsdrgfld  20707  cntzsdrg  20711  abvge0  20726  srngcnv  20756  lmhmlin  20942  lmimf1o  20970  lvecdrng  21012  lspsolvlem  21052  islbs3  21065  lbsextlem3  21070  2idlelbas  21174  2idlcpblrng  21181  zringunit  21376  prmirredlem  21382  irinitoringc  21389  znidomb  21471  cygzn  21480  psgndiflemB  21509  pjf  21622  frlmsslsp  21705  frlmlbs  21706  f1lindf  21731  assalem  21766  psrbaglefi  21835  psrbagleadd1  21837  mplelsfi  21904  mplsubrglem  21913  mplcoe1  21944  mplbas2  21949  opsrtoslem2  21963  mhpmulcl  22036  psdmul  22053  coe1mul2  22155  pmatcoe1fsupp  22588  toponuni  22801  tpsuni  22823  mretopd  22979  neips  23000  neiptoptop  23018  neiptopnei  23019  perflp  23041  perfi  23042  cnf  23133  cnpf  23134  cnpimaex  23143  cnima  23152  t0sep  23211  t1ficld  23214  hausnei  23215  pnrmcld  23229  cnrmi  23247  cmpcov  23276  tgcmp  23288  hauscmplem  23293  connclo  23302  1stcclb  23331  2ndcdisj  23343  llyi  23361  nllyi  23362  ptpjpre1  23458  ptpjcn  23498  ptpjopn  23499  ptclsg  23502  dfac14  23505  txdis1cn  23522  pthaus  23525  hauseqlcld  23533  txkgen  23539  xkococn  23547  txconn  23576  hmeocnvcn  23648  fbssfi  23724  filss  23740  uffixfr  23810  flimneiss  23853  flimelbas  23855  flimfnfcls  23915  alexsubb  23933  alexsubALT  23938  ptcmplem2  23940  ptcmplem3  23941  ptcmplem4  23942  tmdgsum2  23983  ghmcnp  24002  tgpt0  24006  qustgplem  24008  istdrg2  24065  vscacn  24073  tvctdrg  24080  uspreg  24161  ucncn  24172  neipcfilu  24183  cuspcvg  24188  psmetxrge0  24201  isxmet2d  24215  prdsxmetlem  24256  imasdsf1olem  24261  xmstopn  24339  mstopn  24340  stdbdxmet  24403  prdsxmslem2  24417  nrgabv  24549  nmvs  24564  nvclvec  24585  nmoge0  24609  nghmcl  24615  nmoi  24616  nghmghm  24622  nmhmlmhm  24637  nmhmnghm  24638  icccmp  24714  xrge0gsumle  24722  metds0  24739  metdstri  24740  metdsre  24742  metdseq0  24743  metdscnlem  24744  metnrmlem1a  24747  icopnfcnv  24840  xrhmeo  24844  pcoval1  24913  cvslvec  25025  cvsunit  25031  recvs  25046  cphreccllem  25078  cphsscph  25151  cmetcvg  25185  lmle  25201  cmscmet  25246  cmetcusp1  25253  hlcph  25264  minveclem4  25332  ivthlem3  25354  ovolmge0  25378  ovolicc1  25417  ovolicc2lem3  25420  ovolicc2lem5  25422  dyadmbl  25501  i1ff  25577  i1frn  25578  i1fima2  25580  itg2monolem1  25651  dvnres  25833  c1liplem1  25901  c1lip2  25903  dvge0  25911  lhop1lem  25918  itgsubstlem  25955  fta1glem2  26074  fta1b  26077  idomrootle  26078  plyf  26103  plypf1  26117  plyadd  26122  plymul  26123  coeeu  26130  dgrlem  26134  coeid  26143  elqaalem3  26229  aareccl  26234  eff1olem  26457  relogf1o  26475  logdmn0  26549  logcnlem2  26552  logcnlem3  26553  efopnlem1  26565  efopnlem2  26566  logtayl2  26571  cxpcn3lem  26657  cxpcn3  26658  logbgcd1irr  26704  atandmneg  26816  atandmcj  26819  efiatan2  26827  cosatan  26831  cosatanne0  26832  dvatan  26845  areage0  26873  cxp2lim  26887  jensenlem2  26898  jensen  26899  eldmgm  26932  dmgmaddn0  26933  dmlogdmgm  26934  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgambdd  26947  lgamucov  26948  ftalem3  26985  efnnfsumcl  27013  efchtdvds  27069  sqff1o  27092  fsumdvdsdiaglem  27093  dvdsppwf1o  27096  dvdsflf1o  27097  musum  27101  muinv  27103  mpodvdsmulf1o  27104  dvdsmulf1o  27106  lgsfle1  27217  lgsle1  27223  lgsdirprm  27242  lgsne0  27246  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  chebbnd1  27383  chtppilim  27386  chpchtlim  27390  chpo1ub  27391  dchrmusumlema  27404  dchrvmasumlem1  27406  dchrisum0lema  27425  dchrisum0lem2a  27428  logsqvma  27453  selberg3lem2  27469  pntrsumo1  27476  pnt2  27524  ostthlem1  27538  ostth3  27549  sltval2  27568  leftlt  27775  rightgt  27776  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  elons2  28159  onsleft  28161  sltonold  28162  onscutleft  28164  onscutlt  28165  axtgcgrrflx  28389  axtgcgrid  28390  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  tglng  28473  axcontlem7  28897  axcontlem10  28900  upgrle  29017  umgredg2  29027  lfgredgge2  29051  usgredg2ALT  29120  usgr1vr  29182  usgrexmpledg  29189  upgrres1  29240  fusgrvtxfi  29246  vtxnbuvtx  29318  cusgrcplgr  29347  vdumgr0  29408  vtxdgoddnumeven  29481  trlres  29628  usgr2pth  29694  cyclispthon  29734  clwwlknlen  29961  clwwnonrepclwwnon  30274  2clwwlk2  30277  ablocom  30477  phpar2  30752  cbncms  30794  hlph  30818  hcaucvg  31115  hlimconvi  31120  shaddcl  31146  shmulcl  31147  chlimi  31163  chcompl  31171  choc1  31256  nmopre  31799  cnopc  31842  lnopl  31843  unop  31844  hmop  31851  cnfnc  31859  lnfnl  31860  nlelshi  31989  cnlnadjlem5  32000  elpjidm  32113  mdslle1i  32246  mdslle2i  32247  atcv0  32271  chpssati  32292  aciunf1lem  32586  padct  32643  ssnnssfz  32710  ccatf1  32870  swrdrndisj  32879  ressprs  32890  resspos  32892  resstos  32893  pwrssmgc  32926  ogrpinv0le  33029  ogrpsub  33030  ogrpaddlt  33031  wrdpmtrlast  33050  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  isarchi3  33141  archirng  33142  archirngz  33143  archiabllem1a  33145  archiabllem1b  33146  archiabllem2a  33148  archiabllem2c  33149  archiabllem2b  33150  archiabl  33152  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrun  33200  isdrng4  33245  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  ofldtos  33289  ofldlt1  33291  ofldchr  33292  suborng  33293  subofld  33294  isarchiofld  33295  nn0omnd  33316  quslsm  33376  nsgmgclem  33382  nsgmgc  33383  prmidl0  33421  qsidomlem1  33423  mxidlirred  33443  krull  33450  ufdprmidl  33512  1arithufdlem4  33518  sradrng  33578  extdg1id  33661  ply1annnr  33693  madjusmdetlem4  33820  qtophaus  33826  crefi  33837  cmpcref  33840  cmppcmp  33848  pcmplfin  33850  zart0  33869  tpr2rico  33902  rge0scvg  33939  zrhunitpreima  33966  qqhrhm  33979  esummono  34044  gsumesum  34049  esumrnmpt2  34058  esumpinfval  34063  esumpcvgval  34068  esumpmono  34069  0elsiga  34104  sigaclcu  34107  issgon  34113  inelpisys  34144  ldsysgenld  34150  ldgenpisyslem1  34153  sxuni  34183  isrnmeas  34190  measvuni  34204  measssd  34205  ddemeas  34226  imambfm  34253  elmbfmvol2  34258  dya2icoseg2  34269  omssubaddlem  34290  omssubadd  34291  carsgsigalem  34306  pmeasmono  34315  sibfinima  34330  oddpwdc  34345  oddpwdcv  34346  eulerpartlemf  34361  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemgvv  34367  eulerpartlemgs2  34371  fiblem  34389  probtot  34403  ballotlem4  34490  ballotlem5  34491  ballotlemfrc  34518  ballotlemirc  34523  ballotth  34529  hgt750lemb  34647  bnj642  34738  bnj643  34739  bnj645  34740  bnj707  34745  bnj1379  34820  bnj1538  34845  bnj110  34848  bnj93  34853  bnj906  34920  bnj1006  34950  bnj1110  34972  bnj1121  34975  bnj1204  35002  bnj1321  35017  bnj1364  35018  bnj1398  35024  bnj1450  35040  bnj1312  35048  bnj1501  35057  bnj1523  35061  0nn0m1nnn0  35100  subfacp1lem3  35169  subfacp1lem5  35171  pconncn  35211  connpconn  35222  cvmcov  35250  cvmliftlem1  35272  cvmliftlem10  35281  cvmlift2lem11  35300  cvmlift2lem12  35301  msubff1  35543  mvhf1  35546  mthmpps  35569  mclspps  35571  fundmpss  35754  funpartfun  35931  fnetg  36333  neibastop1  36347  filnetlem3  36368  onint1  36437  weiunlem2  36451  weiunpo  36453  weiunse  36456  bj-nnfa  36716  bj-idres  37148  bj-rvecrr  37285  icorempo  37339  pibt2  37405  wl-nfeqfb  37524  phpreu  37598  fin2solem  37600  fin2so  37601  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  ptrest  37613  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  mblfinlem2  37652  dvtan  37664  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  cover2  37709  indexa  37727  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  totbndss  37771  equivtotbnd  37772  isbnd3  37778  totbndbnd  37783  equivbnd  37784  prdsbnd  37787  prdstotbnd  37788  heibor  37815  zrdivrng  37947  crngocom  37995  isfld2  37999  dmncrng  38050  eqvrelrel  38588  disjrel  38722  disjdmqscossss  38795  prter2  38874  toycom  38966  lsateln0  38988  lpssat  39006  lssat  39009  oposlem  39175  olop  39207  omllaw  39236  cvlexch1  39321  dihpN  41330  mapdordlem2  41631  linvh  42084  idomnnzpownz  42120  idomnnzgmulnz  42121  aks6d1c5lem2  42126  deg1pow  42129  redvmptabs  42348  readvrec2  42349  readvrec  42350  mhphflem  42584  prjspertr  42593  nacsfg  42693  nacsfix  42700  mzpindd  42734  diophrw  42747  diophrex  42763  rexzrexnn0  42792  pell1234qrdich  42849  rmspecnonsq  42895  rmspecfund  42897  rmspecpos  42905  monotoddzzfi  42931  ltrmxnn0  42938  rmxnn  42940  jm2.23  42985  jm3.1lem2  43007  dnnumch3  43036  lnmlssfg  43069  lnmlmic  43077  lnrlnm  43102  lnr2i  43105  lpirlnr  43106  hbtlem6  43118  hbt  43119  mnccoe  43127  proot1mul  43183  proot1hash  43184  deg1mhm  43189  ondif1i  43251  limnsuc  43254  cantnfresb  43313  succlg  43317  ntrneifv2  44069  grucollcld  44249  mnurndlem1  44270  ismnushort  44290  radcnvrat  44303  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  ordelordALT  44527  2uasbanh  44551  ordelordALTVD  44856  relprel  44941  elixpconstg  45083  rabidim2  45096  disjinfi  45186  supminfxr2  45465  sumnnodd  45628  stoweidlem7  46005  stoweidlem14  46012  stoweidlem16  46014  stoweidlem24  46022  stoweidlem31  46029  stoweidlem54  46052  wallispilem3  46065  fourierdlem42  46147  fourierdlem48  46152  fourierdlem51  46155  fourierdlem64  46168  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem87  46191  etransclem28  46260  etransclem32  46264  sge0fodjrnlem  46414  hoidmvlelem3  46595  ovolval5lem3  46652  pimrecltpos  46706  pimrecltneg  46722  issmflem  46725  smfaddlem1  46761  smfsuplem1  46809  smfsuplem3  46811  smflimsuplem7  46824  smfliminflem  46828  tworepnotupword  46884  nfunsnafv  47143  faovcl  47201  tz6.12-2-afv2  47238  tz6.12i-afv2  47244  sprel  47485  evendiv2z  47633  oddp1div2z  47634  2dvdseven  47654  2ndvdsodd  47656  perfectALTVlem1  47722  sbgoldbm  47785  upgrimtrls  47906  upgrimpthslem1  47907  upgrimspths  47910  upgrimcycls  47911  uhgrimisgrgric  47931  gpgprismgr4cycllem2  48086  clintopcllaw  48199  uzlidlring  48223  rngccatidALTV  48260  funcringcsetcALTV2lem7  48284  ringccatidALTV  48294  ringcinvALTV  48298  funcringcsetclem7ALTV  48307  fldhmsubcALTV  48321  ssnn0ssfz  48337  el0ldepsnzr  48456  regt1loggt0  48525  elbigodm  48544  fllogbd  48549  rrx2xpref1o  48707  unilbss  48806  fdomne0  48838  f002  48842  xpco2  48845  imaf1homlem  49096  idemb  49148  uobeq2  49390  thincmo2  49415  thincmoALT  49418  fullthinc  49439  idfudiag1  49514  elsetrecslem  49688