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  1520  eumo  2575  reurmo  3351  pssne  4050  pssn2lp  4055  ssnpss  4057  eldifn  4083  elinel2  4153  rabsnt  4685  eldifsni  4743  unimax  4897  ssintub  4918  moop2  5447  pwssun  5513  weso  5612  opelxp2  5664  predpo  6278  frpoinsg  6298  ordwe  6327  funmo  6505  funopg  6523  funun  6535  fununi  6564  funimaexg  6576  fndm  6592  frn  6666  f1ss  6732  f1ssr  6733  forn  6746  f1f1orn  6782  f1orescnv  6786  f1imacnv  6787  funcocnv2  6796  dffv2  6926  exfo  7047  foelrn  7049  foelrnf  7050  isorel  7269  isoini2  7282  f1ofveu  7349  fovcld  7482  onminesb  7735  onminsb  7736  tfisg  7793  tfis  7794  limomss  7810  nnlim  7819  ssnlim  7825  resf1ext2b  7874  curry1  8043  curry2  8046  f1o2ndf1  8061  fnwelem  8070  mpoxopn0yelv  8152  tz7.48lem  8369  dif20el  8429  oeordi  8511  oeeulem  8525  oeeui  8526  nnawordex  8561  swoer  8662  eceqoveq  8755  mapsnconst  8825  resixpfo  8869  boxcutc  8874  sdomnen  8913  en0  8950  en0ALT  8951  en0r  8952  en1  8956  dom0  9028  fodomr  9051  dif1enlem  9079  unxpdomlem3  9152  fineqvlem  9160  infn0  9196  fodomfir  9222  f1opwfi  9250  fsuppcolem  9295  fsuppco  9296  mapfienlem1  9299  mapfienlem2  9300  supub  9353  suplub  9354  ordtypelem2  9415  ordtypelem3  9416  ordtypelem6  9419  ordtypelem7  9420  wemapso2lem  9448  wdom2d  9476  brwdom3  9478  ixpiunwdom  9486  inf3lem2  9529  inf3lem6  9533  oancom  9551  infdifsn  9557  cantnfp1lem3  9580  cantnflem3  9591  cantnflem4  9592  oef1o  9598  cnfcom3  9604  tctr  9638  frinsg  9654  tz9.12lem3  9692  scottex  9788  cardid2  9856  infxpenlem  9914  acni3  9948  cardaleph  9990  iscard3  9994  dfac5lem4  10027  dfac5lem5  10028  dfac5lem4OLD  10029  kmlem1  10052  cofsmo  10170  fin4en1  10210  enfin2i  10222  fin23lem28  10241  fin23lem38  10250  isf32lem6  10259  enfin1ai  10285  hsmexlem2  10328  hsmexlem4  10330  domtriomlem  10343  axdc2lem  10349  axdc3lem2  10352  ac6num  10380  zorn2lem2  10398  brdom3  10429  alephval2  10473  alephreg  10483  pwcfsdom  10484  smobeth  10487  fpwwe2lem5  10536  fpwwe2lem12  10543  canthp1lem2  10554  pwfseqlem3  10561  hargch  10574  winalim2  10597  gchina  10600  inar1  10676  0npi  10783  mulclpi  10794  mulcanpi  10801  nlt1pi  10807  nqereu  10830  prcdnq  10894  prnmax  10896  ltresr2  11042  axrnegex  11063  axpre-sup  11070  eluz2gt1  12828  1nuz2  12832  zsupss  12845  rpgt0  12913  ixxss1  13273  ixxss2  13274  ixxss12  13275  lbioo  13286  ubioo  13287  iccss2  13327  iccssico2  13330  elfzuz3  13431  serge0  13973  expge0  14015  expge1  14016  expaddzlem  14022  hashrabsn1  14291  hashfun  14354  cshinj  14728  relexpuzrel  14969  shftfn  14990  01sqrexlem6  15164  rlimss  15419  lo1dm  15436  o1dm  15447  rlimrege0  15496  fsumf1o  15640  fsumge0  15712  incexc2  15755  supcvg  15773  fprodf1o  15863  divalglem9  16322  bitsfzolem  16355  bitsf1  16367  gcdcllem1  16420  bezout  16464  nprm  16609  dvdsprm  16624  coprm  16632  dfphi2  16695  phimullem  16700  phisum  16712  expnprm  16824  prmreclem2  16839  prmreclem5  16842  1arith  16849  4sqlem18  16884  vdwnnlem3  16919  ramtlecl  16922  rami  16937  0ram  16942  ramub1lem1  16948  prmgaplem5  16977  acsfiel  17570  isacs1i  17573  catlid  17599  catrid  17600  fullfo  17831  fthf1  17836  fthoppc  17842  invfuc  17894  prslem  18213  oduprs  18216  posi  18233  tleile  18335  resspos  18345  resstos  18346  dlatmjdi  18439  pslem  18488  tsrlin  18501  cnvtsr  18504  tsrdir  18520  mndid  18662  mhmf  18707  mhmlin  18711  mhm0  18712  mndind  18746  grpinvex  18866  grplinv  18912  mulgz  19025  mulgdirlem  19028  mulgdir  19029  mulgass  19034  nsgbi  19079  nmzbi  19086  ghmf  19142  ghmlin  19143  conjnsg  19176  gimf1o  19185  gagrpid  19216  gaf  19217  gaass  19219  psgnunilem5  19416  odid  19460  odf1o2  19495  gexid  19503  sylow1lem4  19523  pj1id  19621  efgredeu  19674  ablcmn  19709  cmncom  19720  mulgdi  19748  torsubg  19776  cyggenod2  19807  cygctb  19814  ghmcyg  19818  dprdf1o  19956  ablfacrplem  19989  ablfaclem2  20010  ablfac2  20013  simpg2nsg  20020  fincygsubgodexd  20037  ogrpinv0le  20058  ogrpsub  20059  ogrpaddlt  20060  crngmgp  20169  rnghmmgmhm  20371  rhmmhm  20407  rhmghm  20411  rimf1o  20420  nzrnz  20440  0ringbas  20453  subrgss  20497  subrg1cl  20505  rnghmsubcsetclem1  20556  zrinitorngc  20567  zrtermorngc  20568  rhmsubcsetclem1  20585  ringcinv  20596  zrtermoringc  20600  rrgeq0i  20624  domneq0  20633  domnrrg  20638  drngunit  20659  fldcrngd  20667  drngmgp  20670  drngid  20671  drngdomn  20674  issubdrg  20705  fldhmsubc  20710  fldsdrgfld  20723  cntzsdrg  20727  abvge0  20742  srngcnv  20772  orngsqr  20791  ornglmulle  20792  orngrmulle  20793  ofldtos  20798  ofldlt1  20800  suborng  20801  subofld  20802  lmhmlin  20979  lmimf1o  21007  lvecdrng  21049  lspsolvlem  21089  islbs3  21102  lbsextlem3  21107  2idlelbas  21211  2idlcpblrng  21218  zringunit  21413  prmirredlem  21419  irinitoringc  21426  znidomb  21508  cygzn  21517  ofldchr  21523  psgndiflemB  21547  pjf  21660  frlmsslsp  21743  frlmlbs  21744  f1lindf  21769  assalem  21804  psrbaglefi  21873  psrbagleadd1  21875  mplelsfi  21942  mplsubrglem  21951  mplcoe1  21982  mplbas2  21987  opsrtoslem2  22001  mhpmulcl  22074  psdmul  22091  coe1mul2  22193  pmatcoe1fsupp  22626  toponuni  22839  tpsuni  22861  mretopd  23017  neips  23038  neiptoptop  23056  neiptopnei  23057  perflp  23079  perfi  23080  cnf  23171  cnpf  23172  cnpimaex  23181  cnima  23190  t0sep  23249  t1ficld  23252  hausnei  23253  pnrmcld  23267  cnrmi  23285  cmpcov  23314  tgcmp  23326  hauscmplem  23331  connclo  23340  1stcclb  23369  2ndcdisj  23381  llyi  23399  nllyi  23400  ptpjpre1  23496  ptpjcn  23536  ptpjopn  23537  ptclsg  23540  dfac14  23543  txdis1cn  23560  pthaus  23563  hauseqlcld  23571  txkgen  23577  xkococn  23585  txconn  23614  hmeocnvcn  23686  fbssfi  23762  filss  23778  uffixfr  23848  flimneiss  23891  flimelbas  23893  flimfnfcls  23953  alexsubb  23971  alexsubALT  23976  ptcmplem2  23978  ptcmplem3  23979  ptcmplem4  23980  tmdgsum2  24021  ghmcnp  24040  tgpt0  24044  qustgplem  24046  istdrg2  24103  vscacn  24111  tvctdrg  24118  uspreg  24198  ucncn  24209  neipcfilu  24220  cuspcvg  24225  psmetxrge0  24238  isxmet2d  24252  prdsxmetlem  24293  imasdsf1olem  24298  xmstopn  24376  mstopn  24377  stdbdxmet  24440  prdsxmslem2  24454  nrgabv  24586  nmvs  24601  nvclvec  24622  nmoge0  24646  nghmcl  24652  nmoi  24653  nghmghm  24659  nmhmlmhm  24674  nmhmnghm  24675  icccmp  24751  xrge0gsumle  24759  metds0  24776  metdstri  24777  metdsre  24779  metdseq0  24780  metdscnlem  24781  metnrmlem1a  24784  icopnfcnv  24877  xrhmeo  24881  pcoval1  24950  cvslvec  25062  cvsunit  25068  recvs  25083  cphreccllem  25115  cphsscph  25188  cmetcvg  25222  lmle  25238  cmscmet  25283  cmetcusp1  25290  hlcph  25301  minveclem4  25369  ivthlem3  25391  ovolmge0  25415  ovolicc1  25454  ovolicc2lem3  25457  ovolicc2lem5  25459  dyadmbl  25538  i1ff  25614  i1frn  25615  i1fima2  25617  itg2monolem1  25688  dvnres  25870  c1liplem1  25938  c1lip2  25940  dvge0  25948  lhop1lem  25955  itgsubstlem  25992  fta1glem2  26111  fta1b  26114  idomrootle  26115  plyf  26140  plypf1  26154  plyadd  26159  plymul  26160  coeeu  26167  dgrlem  26171  coeid  26180  elqaalem3  26266  aareccl  26271  eff1olem  26494  relogf1o  26512  logdmn0  26586  logcnlem2  26589  logcnlem3  26590  efopnlem1  26602  efopnlem2  26603  logtayl2  26608  cxpcn3lem  26694  cxpcn3  26695  logbgcd1irr  26741  atandmneg  26853  atandmcj  26856  efiatan2  26864  cosatan  26868  cosatanne0  26869  dvatan  26882  areage0  26910  cxp2lim  26924  jensenlem2  26935  jensen  26936  eldmgm  26969  dmgmaddn0  26970  dmlogdmgm  26971  lgamgulmlem2  26977  lgamgulmlem3  26978  lgamgulmlem5  26980  lgambdd  26984  lgamucov  26985  ftalem3  27022  efnnfsumcl  27050  efchtdvds  27106  sqff1o  27129  fsumdvdsdiaglem  27130  dvdsppwf1o  27133  dvdsflf1o  27134  musum  27138  muinv  27140  mpodvdsmulf1o  27141  dvdsmulf1o  27143  lgsfle1  27254  lgsle1  27260  lgsdirprm  27279  lgsne0  27283  lgseisenlem3  27325  lgseisenlem4  27326  lgsquadlem1  27328  lgsquadlem2  27329  chebbnd1  27420  chtppilim  27423  chpchtlim  27427  chpo1ub  27428  dchrmusumlema  27441  dchrvmasumlem1  27443  dchrisum0lema  27462  dchrisum0lem2a  27465  logsqvma  27490  selberg3lem2  27506  pntrsumo1  27513  pnt2  27561  ostthlem1  27575  ostth3  27586  sltval2  27605  leftlt  27818  rightgt  27819  precsexlem8  28162  precsexlem9  28163  precsexlem11  28165  elons2  28205  onsleft  28207  sltonold  28208  onscutleft  28210  onscutlt  28211  axtgcgrrflx  28450  axtgcgrid  28451  axtgsegcon  28452  axtg5seg  28453  axtgbtwnid  28454  axtgpasch  28455  axtgcont1  28456  tglng  28534  axcontlem7  28959  axcontlem10  28962  upgrle  29079  umgredg2  29089  lfgredgge2  29113  usgredg2ALT  29182  usgr1vr  29244  usgrexmpledg  29251  upgrres1  29302  fusgrvtxfi  29308  vtxnbuvtx  29380  cusgrcplgr  29409  vdumgr0  29470  vtxdgoddnumeven  29543  trlres  29688  usgr2pth  29753  cyclispthon  29793  clwwlknlen  30023  clwwnonrepclwwnon  30336  2clwwlk2  30339  ablocom  30539  phpar2  30814  cbncms  30856  hlph  30880  hcaucvg  31177  hlimconvi  31182  shaddcl  31208  shmulcl  31209  chlimi  31225  chcompl  31233  choc1  31318  nmopre  31861  cnopc  31904  lnopl  31905  unop  31906  hmop  31913  cnfnc  31921  lnfnl  31922  nlelshi  32051  cnlnadjlem5  32062  elpjidm  32175  mdslle1i  32308  mdslle2i  32309  atcv0  32333  aciunf1lem  32655  padct  32712  ssnnssfz  32781  ccatf1  32941  swrdrndisj  32949  ressprs  32958  pwrssmgc  32992  wrdpmtrlast  33073  cyc3evpm  33130  cycpmgcl  33133  cycpmconjslem2  33135  cyc3conja  33137  isarchi3  33167  archirng  33168  archirngz  33169  archiabllem1a  33171  archiabllem1b  33172  archiabllem2a  33174  archiabllem2c  33175  archiabllem2b  33176  archiabl  33178  isarchiofld  33179  elrgspnlem1  33220  elrgspnlem2  33221  elrgspnlem4  33223  elrgspnsubrun  33227  isdrng4  33272  nn0omnd  33320  quslsm  33381  nsgmgclem  33387  nsgmgc  33388  prmidl0  33426  qsidomlem1  33428  mxidlirred  33448  krull  33455  ufdprmidl  33517  1arithufdlem4  33523  mplvrpmlem  33584  mplvrpmga  33586  sradrng  33605  extdg1id  33690  ply1annnr  33727  madjusmdetlem4  33854  qtophaus  33860  crefi  33871  cmpcref  33874  cmppcmp  33882  pcmplfin  33884  zart0  33903  tpr2rico  33936  rge0scvg  33973  zrhunitpreima  34000  qqhrhm  34013  esummono  34078  gsumesum  34083  esumrnmpt2  34092  esumpinfval  34097  esumpcvgval  34102  esumpmono  34103  0elsiga  34138  sigaclcu  34141  issgon  34147  inelpisys  34178  ldsysgenld  34184  ldgenpisyslem1  34187  sxuni  34217  isrnmeas  34224  measvuni  34238  measssd  34239  ddemeas  34260  imambfm  34286  elmbfmvol2  34291  dya2icoseg2  34302  omssubaddlem  34323  omssubadd  34324  carsgsigalem  34339  pmeasmono  34348  sibfinima  34363  oddpwdc  34378  oddpwdcv  34379  eulerpartlemf  34394  eulerpartlemt  34395  eulerpartlemr  34398  eulerpartlemgvv  34400  eulerpartlemgs2  34404  fiblem  34422  probtot  34436  ballotlem4  34523  ballotlem5  34524  ballotlemfrc  34551  ballotlemirc  34556  ballotth  34562  hgt750lemb  34680  bnj642  34771  bnj643  34772  bnj645  34773  bnj707  34778  bnj1379  34853  bnj1538  34878  bnj110  34881  bnj93  34886  bnj906  34953  bnj1006  34983  bnj1110  35005  bnj1121  35008  bnj1204  35035  bnj1321  35050  bnj1364  35051  bnj1398  35057  bnj1450  35073  bnj1312  35081  bnj1501  35090  bnj1523  35094  tz9.1regs  35141  0nn0m1nnn0  35168  subfacp1lem3  35237  subfacp1lem5  35239  pconncn  35279  connpconn  35290  cvmcov  35318  cvmliftlem1  35340  cvmliftlem10  35349  cvmlift2lem11  35368  cvmlift2lem12  35369  msubff1  35611  mvhf1  35614  mthmpps  35637  mclspps  35639  fundmpss  35822  funpartfun  35998  fnetg  36400  neibastop1  36414  filnetlem3  36435  onint1  36504  weiunlem2  36518  weiunpo  36520  weiunse  36523  bj-nnfa  36783  bj-idres  37215  bj-rvecrr  37352  icorempo  37406  pibt2  37472  wl-nfeqfb  37591  phpreu  37654  fin2solem  37656  fin2so  37657  lindsenlbs  37665  matunitlindflem1  37666  matunitlindflem2  37667  matunitlindf  37668  ptrest  37669  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem4  37674  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem9  37679  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem23  37693  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  poimirlem29  37699  poimirlem31  37701  mblfinlem2  37708  dvtan  37720  itg2gt0cn  37725  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  cover2  37765  indexa  37783  istotbnd3  37821  sstotbnd2  37824  sstotbnd  37825  totbndss  37827  equivtotbnd  37828  isbnd3  37834  totbndbnd  37839  equivbnd  37840  prdsbnd  37843  prdstotbnd  37844  heibor  37871  zrdivrng  38003  crngocom  38051  isfld2  38055  dmncrng  38106  eqvrelrel  38703  disjrel  38838  disjdmqscossss  38911  prter2  38990  toycom  39082  lsateln0  39104  lpssat  39122  lssat  39125  oposlem  39291  olop  39323  omllaw  39352  cvlexch1  39437  dihpN  41445  mapdordlem2  41746  linvh  42199  idomnnzpownz  42235  idomnnzgmulnz  42236  aks6d1c5lem2  42241  deg1pow  42244  redvmptabs  42468  readvrec2  42469  readvrec  42470  mhphflem  42704  prjspertr  42713  nacsfg  42812  nacsfix  42819  mzpindd  42853  diophrw  42866  diophrex  42882  rexzrexnn0  42911  pell1234qrdich  42968  rmspecnonsq  43014  rmspecfund  43016  rmspecpos  43023  monotoddzzfi  43049  ltrmxnn0  43056  rmxnn  43058  jm2.23  43103  jm3.1lem2  43125  dnnumch3  43154  lnmlssfg  43187  lnmlmic  43195  lnrlnm  43220  lnr2i  43223  lpirlnr  43224  hbtlem6  43236  hbt  43237  mnccoe  43245  proot1mul  43301  proot1hash  43302  deg1mhm  43307  ondif1i  43369  limnsuc  43372  cantnfresb  43431  succlg  43435  ntrneifv2  44187  grucollcld  44367  mnurndlem1  44388  ismnushort  44408  radcnvrat  44421  binomcxplemdvbinom  44460  binomcxplemcvg  44461  binomcxplemnotnn0  44463  ordelordALT  44644  2uasbanh  44668  ordelordALTVD  44973  relprel  45058  elixpconstg  45200  rabidim2  45213  disjinfi  45303  supminfxr2  45581  sumnnodd  45744  stoweidlem7  46119  stoweidlem14  46126  stoweidlem16  46128  stoweidlem24  46136  stoweidlem31  46143  stoweidlem54  46166  wallispilem3  46179  fourierdlem42  46261  fourierdlem48  46266  fourierdlem51  46269  fourierdlem64  46282  fourierdlem76  46294  fourierdlem79  46297  fourierdlem81  46299  fourierdlem87  46305  etransclem28  46374  etransclem32  46378  sge0fodjrnlem  46528  hoidmvlelem3  46709  ovolval5lem3  46766  pimrecltpos  46820  pimrecltneg  46836  issmflem  46839  smfaddlem1  46875  smfsuplem1  46923  smfsuplem3  46925  smflimsuplem7  46938  smfliminflem  46942  nfunsnafv  47256  faovcl  47314  tz6.12-2-afv2  47351  tz6.12i-afv2  47357  sprel  47598  evendiv2z  47746  oddp1div2z  47747  2dvdseven  47767  2ndvdsodd  47769  perfectALTVlem1  47835  sbgoldbm  47898  upgrimtrls  48020  upgrimpthslem1  48021  upgrimspths  48024  upgrimcycls  48025  uhgrimisgrgric  48045  gpgprismgr4cycllem2  48210  clintopcllaw  48325  uzlidlring  48349  rngccatidALTV  48386  funcringcsetcALTV2lem7  48410  ringccatidALTV  48420  ringcinvALTV  48424  funcringcsetclem7ALTV  48433  fldhmsubcALTV  48447  ssnn0ssfz  48463  el0ldepsnzr  48582  regt1loggt0  48651  elbigodm  48670  fllogbd  48675  rrx2xpref1o  48833  unilbss  48932  fdomne0  48964  f002  48968  xpco2  48971  imaf1homlem  49222  idemb  49274  uobeq2  49516  thincmo2  49541  thincmoALT  49544  fullthinc  49565  idfudiag1  49640  elsetrecslem  49814