Theorem simprbi 503

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 501	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simplbiim  514  xornan  1549  eumo  2606  reurmo  3372  pssne  4029  pssn2lp  4035  ssnpss  4037  eldifn  4071  elinel2  4102  rabsnt  4692  eldifsni  4753  unimax  4908  ssintub  4929  moop2  5478  pwssun  5547  weso  5646  opelxp2  5698  predpo  6344  frpoinsg  6364  ordwe  6393  funmo  6574  funopg  6594  funun  6606  fununi  6637  funimaexg  6648  fndm  6664  frn  6739  f1ss  6807  f1ssr  6808  forn  6821  f1f1orn  6858  f1orescnv  6862  f1imacnv  6863  funcocnv2  6872  funcocnv2OLD  6873  dffv2  7003  exfo  7129  foelrn  7131  foelrnf  7132  isorel  7357  isoini2  7370  f1ofveu  7437  fovcld  7570  onminesb  7831  onminsb  7832  tfisg  7889  tfis  7890  limomss  7906  nnlim  7915  ssnlim  7921  resf1ext2b  7971  curry1  8142  curry2  8145  f1o2ndf1  8160  fnwelem  8170  mpoxopn0yelv  8258  tz7.48lem  8478  tz7.48lemOLD  8479  dif20el  8541  oeordi  8624  oeeulem  8638  oeeui  8639  nnawordex  8674  swoer  8777  eceqoveq  8871  mapsnconst  8948  resixpfo  8992  boxcutc  8997  sdomnen  9036  en0  9073  en0ALT  9074  en0r  9075  en1  9079  dom0  9152  fodomr  9175  dif1enlem  9203  unxpdomlem3  9277  fineqvlem  9285  infn0  9322  fodomfir  9347  f1opwfi  9373  fsuppcolem  9420  fsuppco  9421  mapfienlem1  9424  mapfienlem2  9425  supub  9478  suplub  9479  ordtypelem2  9540  ordtypelem3  9541  ordtypelem6  9544  ordtypelem7  9545  wemapso2lem  9573  wdom2d  9601  brwdom3  9603  ixpiunwdom  9611  inf3lem2  9657  inf3lem6  9661  oancom  9679  infdifsn  9685  cantnfp1lem3  9708  cantnflem3  9719  cantnflem4  9720  oef1o  9726  cnfcom3  9732  tctr  9766  frinsg  9782  tz9.12lem3  9823  hfelhf  9941  hfsshf  9942  hfun  9945  hfuni  9951  scottex  9960  scottexOLD  9961  cardid2  10061  infxpenlem  10119  acni3  10153  cardaleph  10195  iscard3  10199  dfac5lem4  10232  dfac5lem5  10233  kmlem1  10256  cofsmo  10374  fin4en1  10414  enfin2i  10426  fin23lem28  10445  fin23lem38  10454  isf32lem6  10463  enfin1ai  10489  hsmexlem2  10532  hsmexlem4  10534  domtriomlem  10547  axdc2lem  10553  axdc3lem2  10556  ac6num  10584  zorn2lem2  10602  brdom3  10634  alephval2  10684  alephreg  10694  pwcfsdom  10695  smobeth  10698  fpwwe2lem5  10747  fpwwe2lem12  10754  canthp1lem2  10765  pwfseqlem3  10772  hargch  10785  winalim2  10808  gchina  10811  inar1  10887  0npi  10994  mulclpi  11005  mulcanpi  11012  nlt1pi  11018  nqereu  11041  prcdnq  11105  prnmax  11107  ltresr2  11253  axrnegex  11274  axpre-sup  11281  0nn0m1nnn0  12780  eluz2gt1  13074  1nuz2  13078  zsupss  13091  rpgt0  13160  ixxss1  13521  ixxss2  13522  ixxss12  13523  lbioo  13534  ubioo  13535  iccss2  13575  iccssico2  13578  elfzuz3  13680  serge0  14226  expge0  14268  expge1  14269  expaddzlem  14275  hashrabsn1  14545  hashfun  14609  ccatf1  14763  cshinj  14990  relexpuzrel  15234  shftfn  15255  01sqrexlem6  15443  rlimss  15698  lo1dm  15715  o1dm  15726  rlimrege0  15775  fsumf1o  15918  fsumge0  15991  incexc2  16036  supcvg  16054  fprodf1o  16142  divalglem9  16600  bitsfzolem  16633  bitsf1  16645  gcdcllem1  16698  bezout  16745  nprm  16892  dvdsprm  16908  coprm  16916  dfphi2  16980  phimullem  16985  phisum  16997  expnprm  17109  prmreclem2  17124  prmreclem5  17127  1arith  17134  4sqlem18  17169  vdwnnlem3  17204  ramtlecl  17207  rami  17222  0ram  17227  ramub1lem1  17233  prmgaplem5  17262  acsfiel  17857  isacs1i  17860  catlid  17886  catrid  17887  fullfo  18118  fthf1  18123  fthoppc  18129  invfuc  18181  prslem  18500  oduprs  18503  posi  18520  tleile  18622  resspos  18632  resstos  18633  dlatmjdi  18726  pslem  18775  tsrlin  18788  cnvtsr  18791  tsrdir  18807  mndid  18962  mhmf  19013  mhmlin  19017  mhm0  19018  mndind  19053  grpinvex  19183  grplinv  19229  mulgz  19341  mulgdirlem  19344  mulgdir  19345  mulgass  19350  nsgbi  19396  nmzbi  19403  ghmf  19463  ghmlin  19464  conjnsg  19497  gimf1o  19506  gagrpid  19538  gaf  19539  gaass  19541  psgnunilem5  19738  odid  19782  odf1o2  19817  gexid  19825  sylow1lem4  19845  pj1id  19943  efgredeu  19996  ablcmn  20031  cmncom  20042  mulgdi  20070  torsubg  20098  cyggenod2  20129  cygctb  20136  ghmcyg  20140  dprdf1o  20278  ablfacrplem  20311  ablfaclem2  20332  ablfac2  20335  simpg2nsg  20342  fincygsubgodexd  20359  ogrpinv0le  20380  ogrpsub  20381  ogrpaddlt  20382  crngmgp  20497  rnghmmgmhm  20703  rhmmhm  20740  rhmghm  20744  rimf1o  20759  nzrnz  20795  0ringbas  20809  subrgss  20854  subrg1cl  20862  rnghmsubcsetclem1  20913  zrinitorngc  20924  zrtermorngc  20925  rhmsubcsetclem1  20942  ringcinv  20953  zrtermoringc  20957  rrgeq0i  20981  domneq0  20990  domnrrg  20994  drngunit  21015  isdrng4  21022  fldcrngd  21025  drngmgp  21029  drngid  21030  drngdomn  21033  issubdrg  21067  fldhmsubc  21072  fldsdrgfld  21085  cntzsdrg  21089  abvge0  21104  srngcnv  21134  orngsqr  21153  ornglmulle  21154  orngrmulle  21155  ofldtos  21160  ofldlt1  21162  suborng  21163  subofld  21164  lmhmlin  21340  lmimf1o  21368  lvecdrng  21410  lspsolvlem  21450  islbs3  21463  lbsextlem3  21468  2idlelbas  21588  2idlcpblrng  21595  prmidl0  21664  qsidomlem1  21666  zringunit  21802  prmirredlem  21808  irinitoringc  21815  znidomb  21897  cygzn  21906  ofldchr  21912  psgndiflemB  21936  pjf  22049  frlmsslsp  22132  frlmlbs  22133  f1lindf  22158  lindsenlbs  22187  assalem  22195  psrbaglefi  22264  psrbagleadd1  22266  mplelsfi  22332  mplsubrglem  22341  mplcoe1  22376  mplbas2  22381  opsrtoslem2  22395  mhpmulcl  22500  psdmul  22517  coe1mul2  22618  matunitlindflem1  23024  matunitlindflem2  23025  matunitlindf  23026  pmatcoe1fsupp  23049  toponuni  23262  tpsuni  23284  mretopd  23440  neips  23461  neiptoptop  23479  neiptopnei  23480  perflp  23502  perfi  23503  cnf  23594  cnpf  23595  cnpimaex  23604  cnima  23613  t0sep  23672  t1ficld  23675  hausnei  23676  pnrmcld  23690  cnrmi  23708  cmpcov  23737  tgcmp  23749  hauscmplem  23754  connclo  23763  1stcclb  23792  2ndcdisj  23805  llyi  23823  nllyi  23824  ptpjpre1  23920  ptpjcn  23960  ptpjopn  23961  ptclsg  23964  dfac14  23967  txdis1cn  23984  pthaus  23987  hauseqlcld  23995  txkgen  24001  xkococn  24009  txconn  24038  hmeocnvcn  24110  fbssfi  24186  filss  24202  uffixfr  24272  flimneiss  24315  flimelbas  24317  flimfnfcls  24377  alexsubb  24395  alexsubALT  24400  ptcmplem2  24402  ptcmplem3  24403  ptcmplem4  24404  tmdgsum2  24445  ghmcnp  24464  tgpt0  24468  qustgplem  24470  istdrg2  24527  vscacn  24535  tvctdrg  24542  uspreg  24622  ucncn  24633  neipcfilu  24644  cuspcvg  24649  psmetxrge0  24662  isxmet2d  24676  prdsxmetlem  24717  imasdsf1olem  24722  xmstopn  24800  mstopn  24801  stdbdxmet  24864  prdsxmslem2  24878  nrgabv  25010  nmvs  25025  nvclvec  25046  nmoge0  25070  nghmcl  25076  nmoi  25077  nghmghm  25083  nmhmlmhm  25098  nmhmnghm  25099  icccmp  25175  xrge0gsumle  25183  metds0  25200  metdstri  25201  metdsre  25203  metdseq0  25204  metdscnlem  25205  metnrmlem1a  25208  icopnfcnv  25293  xrhmeo  25297  pcoval1  25364  cvslvec  25476  cvsunit  25482  recvs  25497  cphreccllem  25529  cphsscph  25602  cmetcvg  25636  lmle  25652  cmscmet  25697  cmetcusp1  25704  hlcph  25715  minveclem4  25783  ivthlem3  25804  ovolmge0  25828  ovolicc1  25867  ovolicc2lem3  25870  ovolicc2lem5  25872  dyadmbl  25951  i1ff  26027  i1frn  26028  i1fima2  26030  itg2monolem1  26101  dvnres  26281  c1liplem1  26346  c1lip2  26348  dvge0  26356  lhop1lem  26363  itgsubstlem  26398  fta1glem2  26517  fta1b  26520  idomrootle  26521  plyf  26546  plypf1  26561  plyadd  26566  plymul  26567  coeeu  26574  dgrlem  26578  coeid  26587  elqaalem3  26674  preimaaa  26676  aareccl  26683  eff1olem  26906  relogf1o  26924  logdmn0  26998  logcnlem2  27001  logcnlem3  27002  efopnlem1  27014  efopnlem2  27015  logtayl2  27020  cxpcn3lem  27105  cxpcn3  27106  logbgcd1irr  27152  atandmneg  27264  atandmcj  27267  efiatan2  27275  cosatan  27279  cosatanne0  27280  dvatan  27293  areage0  27321  cxp2lim  27334  jensenlem2  27345  jensen  27346  eldmgm  27379  dmgmaddn0  27380  dmlogdmgm  27381  lgamgulmlem2  27387  lgamgulmlem3  27388  lgamgulmlem5  27390  lgambdd  27394  lgamucov  27395  ftalem3  27432  efnnfsumcl  27460  efchtdvds  27516  sqff1o  27539  fsumdvdsdiaglem  27540  dvdsppwf1o  27543  dvdsflf1o  27544  musum  27548  muinv  27550  mpodvdsmulf1o  27551  dvdsmulf1o  27553  lgsfle1  27663  lgsle1  27669  lgsdirprm  27688  lgsne0  27692  lgseisenlem3  27734  lgseisenlem4  27735  lgsquadlem1  27737  lgsquadlem2  27738  chebbnd1  27829  chtppilim  27832  chpchtlim  27836  chpo1ub  27837  dchrmusumlema  27850  dchrvmasumlem1  27852  dchrisum0lema  27871  dchrisum0lem2a  27874  logsqvma  27899  selberg3lem2  27915  pntrsumo1  27922  pnt2  27970  ostthlem1  27984  ostth3  27995  ltsval2  28043  leftlt  28269  rightgt  28270  precsexlem8  28630  precsexlem9  28631  precsexlem11  28633  elons2  28674  onleft  28676  ltonold  28677  oncutleft  28679  oncutlt  28680  zcuts0  28824  axtgcgrrflx  28954  axtgcgrid  28955  axtgsegcon  28956  axtg5seg  28957  axtgbtwnid  28958  axtgpasch  28959  axtgcont1  28960  tglng  29039  axcontlem7  29578  axcontlem10  29581  upgrle  29698  umgredg2  29708  lfgredgge2  29732  usgredg2ALT  29804  usgr1vr  29866  usgrexmpledg  29873  upgrres1  29924  fusgrvtxfi  29930  vtxnbuvtx  30002  cusgrcplgr  30031  vdumgr0  30091  vtxdgoddnumeven  30164  trlres  30313  pthhashvtx  30345  usgr2pth  30380  cyclispthon  30423  clwwlknlen  30653  clwwnonrepclwwnon  30976  2clwwlk2  30979  ablocom  31180  phpar2  31455  cbncms  31497  hlph  31521  hcaucvg  31818  hlimconvi  31823  shaddcl  31849  shmulcl  31850  chlimi  31866  chcompl  31874  choc1  31959  nmopre  32502  cnopc  32545  lnopl  32546  unop  32547  hmop  32554  cnfnc  32562  lnfnl  32563  nlelshi  32692  cnlnadjlem5  32703  elpjidm  32816  mdslle1i  32949  mdslle2i  32950  atcv0  32974  aciunf1lem  33328  padct  33381  ssnnssfz  33449  swrdrndisj  33588  ressprs  33597  pwrssmgc  33631  wrdpmtrlast  33724  cyc3evpm  33781  cycpmgcl  33784  cycpmconjslem2  33786  cyc3conja  33788  isarchi3  33818  archirng  33819  archirngz  33820  archiabllem1a  33822  archiabllem1b  33823  archiabllem2a  33825  archiabllem2c  33826  archiabllem2b  33827  archiabl  33829  isarchiofld  33830  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem4  33876  elrgspnsubrun  33880  ricnzr1  33919  ricdomn1  33920  nn0omnd  33975  quslsm  34026  nsgmgclem  34032  nsgmgc  34033  mxidlirred  34067  krull  34073  ufdprmidl  34143  1arithufdlem4  34149  extvfvcl  34238  mplvrpmga  34247  sradrng  34284  extdg1id  34368  ply1annnr  34405  madjusmdetlem4  34532  qtophaus  34538  crefi  34549  cmpcref  34552  cmppcmp  34560  pcmplfin  34562  zart0  34581  tpr2rico  34614  rge0scvg  34651  zrhunitpreima  34678  qqhrhm  34691  esummono  34756  gsumesum  34761  esumrnmpt2  34770  esumpinfval  34775  esumpcvgval  34780  esumpmono  34781  0elsiga  34816  sigaclcu  34819  issgon  34825  inelpisys  34857  ldsysgenld  34863  ldgenpisyslem1  34866  sxuni  34896  isrnmeas  34903  measvuni  34917  measssd  34918  ddemeas  34939  imambfm  34964  elmbfmvol2  34969  dya2icoseg2  34980  omssubaddlem  35001  omssubadd  35002  carsgsigalem  35017  pmeasmono  35026  sibfinima  35041  oddpwdc  35056  oddpwdcv  35057  eulerpartlemf  35072  eulerpartlemt  35073  eulerpartlemr  35076  eulerpartlemgvv  35078  eulerpartlemgs2  35082  fiblem  35100  probtot  35114  ballotlem4  35201  ballotlem5  35202  ballotlemfrc  35229  ballotlemirc  35234  ballotth  35240  hgt750lemb  35355  bnj642  35449  bnj643  35450  bnj645  35451  bnj707  35456  bnj1379  35530  bnj1538  35555  bnj110  35558  bnj93  35563  bnj906  35630  bnj1006  35660  bnj1110  35682  bnj1121  35685  bnj1204  35712  bnj1321  35727  bnj1364  35728  bnj1398  35734  bnj1450  35750  bnj1312  35758  bnj1501  35767  bnj1523  35771  f1preimaex  35785  soinfdom  35800  elscottrank  35829  elscottrankss  35831  tz9.1regs  35902  onprcf1acwevdlem2  36046  onvfowev  36050  onprcf1of1ord  36055  subfacp1lem3  36114  subfacp1lem5  36116  pconncn  36156  connpconn  36167  cvmcov  36195  cvmliftlem1  36217  cvmliftlem10  36226  cvmlift2lem11  36245  cvmlift2lem12  36246  msubff1  36488  mvhf1  36491  mthmpps  36514  mclspps  36516  mirimanofffr  36629  fundmpss  36710  funpartfun  36885  fnetg  37311  neibastop1  37325  filnetlem3  37346  onint1  37415  weiunlem  37429  weiunpo  37431  weiunse  37434  bj-nnfa  37808  bj-idres  38273  bj-rvecrr  38410  icorempo  38466  pibt2  38532  wl-nfeqfb  38660  phpreu  38719  fin2solem  38721  fin2so  38722  ptrest  38729  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem9  38739  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem14  38744  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem23  38753  poimirlem24  38754  poimirlem26  38756  poimirlem27  38757  poimirlem29  38759  poimirlem31  38761  mblfinlem2  38768  dvtan  38780  itg2gt0cn  38785  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  cover2  38841  indexa  38859  istotbnd3  38897  sstotbnd2  38900  sstotbnd  38901  totbndss  38903  equivtotbnd  38904  isbnd3  38910  totbndbnd  38915  equivbnd  38916  prdsbnd  38919  prdstotbnd  38920  heibor  38947  zrdivrng  39079  crngocom  39127  isfld2  39131  dmncrng  39182  eqvrelrel  39805  disjrel  39954  disjdmqscossss  40030  prter2  40130  toycom  40222  lsateln0  40244  lpssat  40262  lssat  40265  oposlem  40431  olop  40463  omllaw  40492  cvlexch1  40577  dihpN  42585  mapdordlem2  42886  linvh  43338  idomnnzpownz  43374  idomnnzgmulnz  43375  aks6d1c5lem2  43380  deg1pow  43383  redvmptabs  43604  readvrec2  43605  readvrec  43606  mhphflem  43817  prjspertr  43826  nacsfg  43909  nacsfix  43916  mzpindd  43950  diophrw  43963  diophrex  43979  rexzrexnn0  44004  pell1234qrdich  44061  rmspecnonsq  44107  rmspecfund  44109  rmspecpos  44116  monotoddzzfi  44142  ltrmxnn0  44149  rmxnn  44151  jm2.23  44196  jm3.1lem2  44218  dnnumch3  44247  lnmlssfg  44275  lnmlmic  44283  lnrlnm  44307  lnr2i  44310  lpirlnr  44311  hbtlem6  44323  hbt  44324  mnccoe  44332  proot1mul  44388  proot1hash  44389  deg1mhm  44394  ondif1i  44456  limnsuc  44459  cantnfresb  44518  succlg  44522  ntrneifv2  45272  grucollcld  45436  mnurndlem1  45457  ismnushort  45477  radcnvrat  45490  binomcxplemdvbinom  45529  binomcxplemcvg  45530  binomcxplemnotnn0  45532  ordelordALT  45711  2uasbanh  45735  ordelordALTVD  46040  relprel  46136  elixpconstg  46309  rabidim2  46322  disjinfi  46412  supminfxr2  46684  sumnnodd  46847  stoweidlem7  47222  stoweidlem14  47229  stoweidlem16  47231  stoweidlem24  47239  stoweidlem31  47246  stoweidlem54  47269  wallispilem3  47282  fourierdlem42  47364  fourierdlem48  47369  fourierdlem51  47372  fourierdlem64  47385  fourierdlem76  47397  fourierdlem79  47400  fourierdlem81  47402  fourierdlem87  47408  etransclem28  47477  etransclem32  47481  sge0fodjrnlem  47631  hoidmvlelem3  47812  ovolval5lem3  47869  pimrecltpos  47923  pimrecltneg  47939  issmflem  47942  smfaddlem1  47978  smfsuplem1  48026  smfsuplem3  48028  smflimsuplem7  48041  smfliminflem  48045  chndin  48106  chnrin  48111  nfunsnafv  48417  faovcl  48475  tz6.12-2-afv2  48512  tz6.12i-afv2  48518  sprel  48771  evendiv2z  48935  oddp1div2z  48936  2dvdseven  48956  2ndvdsodd  48958  perfectALTVlem1  49024  sbgoldbm  49087  upgrimtrls  49209  upgrimpthslem1  49210  upgrimspths  49213  upgrimcycls  49214  uhgrimisgrgric  49234  gpgprismgr4cycllem2  49399  clintopcllaw  49513  uzlidlring  49537  rngccatidALTV  49574  funcringcsetcALTV2lem7  49598  ringccatidALTV  49608  ringcinvALTV  49612  funcringcsetclem7ALTV  49621  fldhmsubcALTV  49635  ssnn0ssfz  49666  el0ldepsnzr  49784  regt1loggt0  49853  elbigodm  49872  fllogbd  49877  unilbss  50134  fdomne0  50166  f002  50170  xpco2  50173  imaf1homlem  50428  idemb  50480  uobeq2  50741  thincmo2  50766  thincmoALT  50769  fullthinc  50790  idfudiag1  50865  elsetrecslem  51072  dvsec  51136  dvcsc  51137  dvcot  51138  alseueu  51213