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  2603  reurmo  3368  pssne  4046  pssn2lp  4052  ssnpss  4054  eldifn  4078  elinel2  4147  rabsnt  4691  eldifsni  4752  unimax  4904  ssintub  4925  moop2  5471  pwssun  5539  weso  5638  opelxp2  5690  predpo  6315  frpoinsg  6335  ordwe  6364  funmo  6543  funopg  6562  funun  6574  fununi  6603  funimaexg  6614  fndm  6630  frn  6705  f1ss  6773  f1ssr  6774  forn  6787  f1f1orn  6824  f1orescnv  6828  f1imacnv  6829  funcocnv2  6838  dffv2  6968  exfo  7093  foelrn  7095  foelrnf  7096  isorel  7322  isoini2  7335  f1ofveu  7402  fovcld  7535  onminesb  7790  onminsb  7791  tfisg  7848  tfis  7849  limomss  7865  nnlim  7874  ssnlim  7880  resf1ext2b  7930  curry1  8098  curry2  8101  f1o2ndf1  8116  fnwelem  8126  mpoxopn0yelv  8208  tz7.48lem  8428  tz7.48lemOLD  8429  dif20el  8491  oeordi  8574  oeeulem  8588  oeeui  8589  nnawordex  8624  swoer  8727  eceqoveq  8821  mapsnconst  8898  resixpfo  8942  boxcutc  8947  sdomnen  8986  en0  9023  en0ALT  9024  en0r  9025  en1  9029  dom0  9102  fodomr  9125  dif1enlem  9153  unxpdomlem3  9227  fineqvlem  9235  infn0  9272  fodomfir  9297  f1opwfi  9323  fsuppcolem  9371  fsuppco  9372  mapfienlem1  9375  mapfienlem2  9376  supub  9429  suplub  9430  ordtypelem2  9491  ordtypelem3  9492  ordtypelem6  9495  ordtypelem7  9496  wemapso2lem  9524  wdom2d  9552  brwdom3  9554  ixpiunwdom  9562  inf3lem2  9608  inf3lem6  9612  oancom  9630  infdifsn  9636  cantnfp1lem3  9659  cantnflem3  9670  cantnflem4  9671  oef1o  9677  cnfcom3  9683  tctr  9717  frinsg  9733  tz9.12lem3  9771  hfelhf  9886  hfsshf  9887  hfun  9890  hfuni  9896  scottex  9905  scottexOLD  9906  cardid2  10006  infxpenlem  10064  acni3  10098  cardaleph  10140  iscard3  10144  dfac5lem4  10177  dfac5lem5  10178  kmlem1  10201  cofsmo  10319  fin4en1  10359  enfin2i  10371  fin23lem28  10390  fin23lem38  10399  isf32lem6  10408  enfin1ai  10434  hsmexlem2  10477  hsmexlem4  10479  domtriomlem  10492  axdc2lem  10498  axdc3lem2  10501  ac6num  10529  zorn2lem2  10547  brdom3  10579  alephval2  10629  alephreg  10639  pwcfsdom  10640  smobeth  10643  fpwwe2lem5  10692  fpwwe2lem12  10699  canthp1lem2  10710  pwfseqlem3  10717  hargch  10730  winalim2  10753  gchina  10756  inar1  10832  0npi  10939  mulclpi  10950  mulcanpi  10957  nlt1pi  10963  nqereu  10986  prcdnq  11050  prnmax  11052  ltresr2  11198  axrnegex  11219  axpre-sup  11226  0nn0m1nnn0  12723  eluz2gt1  13017  1nuz2  13021  zsupss  13034  rpgt0  13103  ixxss1  13464  ixxss2  13465  ixxss12  13466  lbioo  13477  ubioo  13478  iccss2  13518  iccssico2  13521  elfzuz3  13623  serge0  14168  expge0  14210  expge1  14211  expaddzlem  14217  hashrabsn1  14486  hashfun  14550  ccatf1  14704  cshinj  14930  relexpuzrel  15173  shftfn  15194  01sqrexlem6  15382  rlimss  15637  lo1dm  15654  o1dm  15665  rlimrege0  15714  fsumf1o  15857  fsumge0  15930  incexc2  15975  supcvg  15993  fprodf1o  16081  divalglem9  16539  bitsfzolem  16572  bitsf1  16584  gcdcllem1  16637  bezout  16681  nprm  16826  dvdsprm  16842  coprm  16850  dfphi2  16913  phimullem  16918  phisum  16930  expnprm  17042  prmreclem2  17057  prmreclem5  17060  1arith  17067  4sqlem18  17102  vdwnnlem3  17137  ramtlecl  17140  rami  17155  0ram  17160  ramub1lem1  17166  prmgaplem5  17195  acsfiel  17790  isacs1i  17793  catlid  17819  catrid  17820  fullfo  18051  fthf1  18056  fthoppc  18062  invfuc  18114  prslem  18433  oduprs  18436  posi  18453  tleile  18555  resspos  18565  resstos  18566  dlatmjdi  18659  pslem  18708  tsrlin  18721  cnvtsr  18724  tsrdir  18740  mndid  18895  mhmf  18946  mhmlin  18950  mhm0  18951  mndind  18986  grpinvex  19116  grplinv  19162  mulgz  19274  mulgdirlem  19277  mulgdir  19278  mulgass  19283  nsgbi  19329  nmzbi  19336  ghmf  19396  ghmlin  19397  conjnsg  19430  gimf1o  19439  gagrpid  19470  gaf  19471  gaass  19473  psgnunilem5  19670  odid  19714  odf1o2  19749  gexid  19757  sylow1lem4  19777  pj1id  19875  efgredeu  19928  ablcmn  19963  cmncom  19974  mulgdi  20002  torsubg  20030  cyggenod2  20061  cygctb  20068  ghmcyg  20072  dprdf1o  20210  ablfacrplem  20243  ablfaclem2  20264  ablfac2  20267  simpg2nsg  20274  fincygsubgodexd  20291  ogrpinv0le  20312  ogrpsub  20313  ogrpaddlt  20314  crngmgp  20429  rnghmmgmhm  20635  rhmmhm  20672  rhmghm  20676  rimf1o  20691  nzrnz  20727  0ringbas  20741  subrgss  20786  subrg1cl  20794  rnghmsubcsetclem1  20845  zrinitorngc  20856  zrtermorngc  20857  rhmsubcsetclem1  20874  ringcinv  20885  zrtermoringc  20889  rrgeq0i  20913  domneq0  20922  domnrrg  20926  drngunit  20947  isdrng4  20954  fldcrngd  20957  drngmgp  20961  drngid  20962  drngdomn  20965  issubdrg  20999  fldhmsubc  21004  fldsdrgfld  21017  cntzsdrg  21021  abvge0  21036  srngcnv  21066  orngsqr  21085  ornglmulle  21086  orngrmulle  21087  ofldtos  21092  ofldlt1  21094  suborng  21095  subofld  21096  lmhmlin  21272  lmimf1o  21300  lvecdrng  21342  lspsolvlem  21382  islbs3  21395  lbsextlem3  21400  2idlelbas  21520  2idlcpblrng  21527  prmidl0  21596  qsidomlem1  21598  zringunit  21734  prmirredlem  21740  irinitoringc  21747  znidomb  21829  cygzn  21838  ofldchr  21844  psgndiflemB  21868  pjf  21981  frlmsslsp  22064  frlmlbs  22065  f1lindf  22090  lindsenlbs  22119  assalem  22127  psrbaglefi  22196  psrbagleadd1  22198  mplelsfi  22264  mplsubrglem  22273  mplcoe1  22308  mplbas2  22313  opsrtoslem2  22327  mhpmulcl  22432  psdmul  22449  coe1mul2  22550  matunitlindflem1  22956  matunitlindflem2  22957  matunitlindf  22958  pmatcoe1fsupp  22981  toponuni  23194  tpsuni  23216  mretopd  23372  neips  23393  neiptoptop  23411  neiptopnei  23412  perflp  23434  perfi  23435  cnf  23526  cnpf  23527  cnpimaex  23536  cnima  23545  t0sep  23604  t1ficld  23607  hausnei  23608  pnrmcld  23622  cnrmi  23640  cmpcov  23669  tgcmp  23681  hauscmplem  23686  connclo  23695  1stcclb  23724  2ndcdisj  23737  llyi  23755  nllyi  23756  ptpjpre1  23852  ptpjcn  23892  ptpjopn  23893  ptclsg  23896  dfac14  23899  txdis1cn  23916  pthaus  23919  hauseqlcld  23927  txkgen  23933  xkococn  23941  txconn  23970  hmeocnvcn  24042  fbssfi  24118  filss  24134  uffixfr  24204  flimneiss  24247  flimelbas  24249  flimfnfcls  24309  alexsubb  24327  alexsubALT  24332  ptcmplem2  24334  ptcmplem3  24335  ptcmplem4  24336  tmdgsum2  24377  ghmcnp  24396  tgpt0  24400  qustgplem  24402  istdrg2  24459  vscacn  24467  tvctdrg  24474  uspreg  24554  ucncn  24565  neipcfilu  24576  cuspcvg  24581  psmetxrge0  24594  isxmet2d  24608  prdsxmetlem  24649  imasdsf1olem  24654  xmstopn  24732  mstopn  24733  stdbdxmet  24796  prdsxmslem2  24810  nrgabv  24942  nmvs  24957  nvclvec  24978  nmoge0  25002  nghmcl  25008  nmoi  25009  nghmghm  25015  nmhmlmhm  25030  nmhmnghm  25031  icccmp  25107  xrge0gsumle  25115  metds0  25132  metdstri  25133  metdsre  25135  metdseq0  25136  metdscnlem  25137  metnrmlem1a  25140  icopnfcnv  25225  xrhmeo  25229  pcoval1  25296  cvslvec  25408  cvsunit  25414  recvs  25429  cphreccllem  25461  cphsscph  25534  cmetcvg  25568  lmle  25584  cmscmet  25629  cmetcusp1  25636  hlcph  25647  minveclem4  25715  ivthlem3  25736  ovolmge0  25760  ovolicc1  25799  ovolicc2lem3  25802  ovolicc2lem5  25804  dyadmbl  25883  i1ff  25959  i1frn  25960  i1fima2  25962  itg2monolem1  26033  dvnres  26213  c1liplem1  26278  c1lip2  26280  dvge0  26288  lhop1lem  26295  itgsubstlem  26330  fta1glem2  26449  fta1b  26452  idomrootle  26453  plyf  26478  plypf1  26493  plyadd  26498  plymul  26499  coeeu  26506  dgrlem  26510  coeid  26519  elqaalem3  26608  preimaaa  26610  aareccl  26617  eff1olem  26840  relogf1o  26858  logdmn0  26932  logcnlem2  26935  logcnlem3  26936  efopnlem1  26948  efopnlem2  26949  logtayl2  26954  cxpcn3lem  27039  cxpcn3  27040  logbgcd1irr  27086  atandmneg  27198  atandmcj  27201  efiatan2  27209  cosatan  27213  cosatanne0  27214  dvatan  27227  areage0  27255  cxp2lim  27268  jensenlem2  27279  jensen  27280  eldmgm  27313  dmgmaddn0  27314  dmlogdmgm  27315  lgamgulmlem2  27321  lgamgulmlem3  27322  lgamgulmlem5  27324  lgambdd  27328  lgamucov  27329  ftalem3  27366  efnnfsumcl  27394  efchtdvds  27450  sqff1o  27473  fsumdvdsdiaglem  27474  dvdsppwf1o  27477  dvdsflf1o  27478  musum  27482  muinv  27484  mpodvdsmulf1o  27485  dvdsmulf1o  27487  lgsfle1  27597  lgsle1  27603  lgsdirprm  27622  lgsne0  27626  lgseisenlem3  27668  lgseisenlem4  27669  lgsquadlem1  27671  lgsquadlem2  27672  chebbnd1  27763  chtppilim  27766  chpchtlim  27770  chpo1ub  27771  dchrmusumlema  27784  dchrvmasumlem1  27786  dchrisum0lema  27805  dchrisum0lem2a  27808  logsqvma  27833  selberg3lem2  27849  pntrsumo1  27856  pnt2  27904  ostthlem1  27918  ostth3  27929  ltsval2  27947  leftlt  28173  rightgt  28174  precsexlem8  28534  precsexlem9  28535  precsexlem11  28537  elons2  28578  onleft  28580  ltonold  28581  oncutleft  28583  oncutlt  28584  zcuts0  28728  axtgcgrrflx  28858  axtgcgrid  28859  axtgsegcon  28860  axtg5seg  28861  axtgbtwnid  28862  axtgpasch  28863  axtgcont1  28864  tglng  28943  axcontlem7  29482  axcontlem10  29485  upgrle  29602  umgredg2  29612  lfgredgge2  29636  usgredg2ALT  29708  usgr1vr  29770  usgrexmpledg  29777  upgrres1  29828  fusgrvtxfi  29834  vtxnbuvtx  29906  cusgrcplgr  29935  vdumgr0  29995  vtxdgoddnumeven  30068  trlres  30217  pthhashvtx  30249  usgr2pth  30284  cyclispthon  30327  clwwlknlen  30557  clwwnonrepclwwnon  30880  2clwwlk2  30883  ablocom  31084  phpar2  31359  cbncms  31401  hlph  31425  hcaucvg  31722  hlimconvi  31727  shaddcl  31753  shmulcl  31754  chlimi  31770  chcompl  31778  choc1  31863  nmopre  32406  cnopc  32449  lnopl  32450  unop  32451  hmop  32458  cnfnc  32466  lnfnl  32467  nlelshi  32596  cnlnadjlem5  32607  elpjidm  32720  mdslle1i  32853  mdslle2i  32854  atcv0  32878  aciunf1lem  33190  padct  33244  ssnnssfz  33313  swrdrndisj  33452  ressprs  33461  pwrssmgc  33495  wrdpmtrlast  33588  cyc3evpm  33645  cycpmgcl  33648  cycpmconjslem2  33650  cyc3conja  33652  isarchi3  33682  archirng  33683  archirngz  33684  archiabllem1a  33686  archiabllem1b  33687  archiabllem2a  33689  archiabllem2c  33690  archiabllem2b  33691  archiabl  33693  isarchiofld  33694  elrgspnlem1  33737  elrgspnlem2  33738  elrgspnlem4  33740  elrgspnsubrun  33744  ricnzr1  33783  ricdomn1  33784  nn0omnd  33839  quslsm  33890  nsgmgclem  33896  nsgmgc  33897  mxidlirred  33931  krull  33937  ufdprmidl  34007  1arithufdlem4  34013  extvfvcl  34102  mplvrpmga  34111  sradrng  34148  extdg1id  34232  ply1annnr  34269  madjusmdetlem4  34396  qtophaus  34402  crefi  34413  cmpcref  34416  cmppcmp  34424  pcmplfin  34426  zart0  34445  tpr2rico  34478  rge0scvg  34515  zrhunitpreima  34542  qqhrhm  34555  esummono  34620  gsumesum  34625  esumrnmpt2  34634  esumpinfval  34639  esumpcvgval  34644  esumpmono  34645  0elsiga  34680  sigaclcu  34683  issgon  34689  inelpisys  34721  ldsysgenld  34727  ldgenpisyslem1  34730  sxuni  34760  isrnmeas  34767  measvuni  34781  measssd  34782  ddemeas  34803  imambfm  34829  elmbfmvol2  34834  dya2icoseg2  34845  omssubaddlem  34866  omssubadd  34867  carsgsigalem  34882  pmeasmono  34891  sibfinima  34906  oddpwdc  34921  oddpwdcv  34922  eulerpartlemf  34937  eulerpartlemt  34938  eulerpartlemr  34941  eulerpartlemgvv  34943  eulerpartlemgs2  34947  fiblem  34965  probtot  34979  ballotlem4  35066  ballotlem5  35067  ballotlemfrc  35094  ballotlemirc  35099  ballotth  35105  hgt750lemb  35220  bnj642  35314  bnj643  35315  bnj645  35316  bnj707  35321  bnj1379  35395  bnj1538  35420  bnj110  35423  bnj93  35428  bnj906  35495  bnj1006  35525  bnj1110  35547  bnj1121  35550  bnj1204  35577  bnj1321  35592  bnj1364  35593  bnj1398  35599  bnj1450  35615  bnj1312  35623  bnj1501  35632  bnj1523  35636  elscottrank  35675  elscottrankss  35677  tz9.1regs  35727  onvfowev  35820  subfacp1lem3  35868  subfacp1lem5  35870  pconncn  35910  connpconn  35921  cvmcov  35949  cvmliftlem1  35971  cvmliftlem10  35980  cvmlift2lem11  35999  cvmlift2lem12  36000  msubff1  36242  mvhf1  36245  mthmpps  36268  mclspps  36270  fundmpss  36453  funpartfun  36629  fnetg  37055  neibastop1  37069  filnetlem3  37090  onint1  37159  weiunlem  37173  weiunpo  37175  weiunse  37178  bj-nnfa  37552  bj-idres  38001  bj-rvecrr  38138  icorempo  38194  pibt2  38260  wl-nfeqfb  38388  phpreu  38447  fin2solem  38449  fin2so  38450  ptrest  38457  poimirlem1  38459  poimirlem2  38460  poimirlem3  38461  poimirlem4  38462  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem9  38467  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem13  38471  poimirlem14  38472  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem18  38476  poimirlem19  38477  poimirlem20  38478  poimirlem21  38479  poimirlem22  38480  poimirlem23  38481  poimirlem24  38482  poimirlem26  38484  poimirlem27  38485  poimirlem29  38487  poimirlem31  38489  mblfinlem2  38496  dvtan  38508  itg2gt0cn  38513  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  cover2  38569  indexa  38587  istotbnd3  38625  sstotbnd2  38628  sstotbnd  38629  totbndss  38631  equivtotbnd  38632  isbnd3  38638  totbndbnd  38643  equivbnd  38644  prdsbnd  38647  prdstotbnd  38648  heibor  38675  zrdivrng  38807  crngocom  38855  isfld2  38859  dmncrng  38910  eqvrelrel  39533  disjrel  39682  disjdmqscossss  39758  prter2  39858  toycom  39950  lsateln0  39972  lpssat  39990  lssat  39993  oposlem  40159  olop  40191  omllaw  40220  cvlexch1  40305  dihpN  42313  mapdordlem2  42614  linvh  43066  idomnnzpownz  43102  idomnnzgmulnz  43103  aks6d1c5lem2  43108  deg1pow  43111  redvmptabs  43339  readvrec2  43340  readvrec  43341  mhphflem  43546  prjspertr  43555  nacsfg  43654  nacsfix  43661  mzpindd  43695  diophrw  43708  diophrex  43724  rexzrexnn0  43749  pell1234qrdich  43806  rmspecnonsq  43852  rmspecfund  43854  rmspecpos  43861  monotoddzzfi  43887  ltrmxnn0  43894  rmxnn  43896  jm2.23  43941  jm3.1lem2  43963  dnnumch3  43992  lnmlssfg  44025  lnmlmic  44033  lnrlnm  44058  lnr2i  44061  lpirlnr  44062  hbtlem6  44074  hbt  44075  mnccoe  44083  proot1mul  44139  proot1hash  44140  deg1mhm  44145  ondif1i  44207  limnsuc  44210  cantnfresb  44269  succlg  44273  ntrneifv2  45024  grucollcld  45188  mnurndlem1  45209  ismnushort  45229  radcnvrat  45242  binomcxplemdvbinom  45281  binomcxplemcvg  45282  binomcxplemnotnn0  45284  ordelordALT  45464  2uasbanh  45488  ordelordALTVD  45793  relprel  45878  elixpconstg  46025  rabidim2  46038  disjinfi  46128  supminfxr2  46401  sumnnodd  46564  stoweidlem7  46939  stoweidlem14  46946  stoweidlem16  46948  stoweidlem24  46956  stoweidlem31  46963  stoweidlem54  46986  wallispilem3  46999  fourierdlem42  47081  fourierdlem48  47086  fourierdlem51  47089  fourierdlem64  47102  fourierdlem76  47114  fourierdlem79  47117  fourierdlem81  47119  fourierdlem87  47125  etransclem28  47194  etransclem32  47198  sge0fodjrnlem  47348  hoidmvlelem3  47529  ovolval5lem3  47586  pimrecltpos  47640  pimrecltneg  47656  issmflem  47659  smfaddlem1  47695  smfsuplem1  47743  smfsuplem3  47745  smflimsuplem7  47758  smfliminflem  47762  chndin  47823  chnrin  47828  nfunsnafv  48134  faovcl  48192  tz6.12-2-afv2  48229  tz6.12i-afv2  48235  sprel  48488  evendiv2z  48652  oddp1div2z  48653  2dvdseven  48673  2ndvdsodd  48675  perfectALTVlem1  48741  sbgoldbm  48804  upgrimtrls  48926  upgrimpthslem1  48927  upgrimspths  48930  upgrimcycls  48931  uhgrimisgrgric  48951  gpgprismgr4cycllem2  49116  clintopcllaw  49230  uzlidlring  49254  rngccatidALTV  49291  funcringcsetcALTV2lem7  49315  ringccatidALTV  49325  ringcinvALTV  49329  funcringcsetclem7ALTV  49338  fldhmsubcALTV  49352  ssnn0ssfz  49383  el0ldepsnzr  49501  regt1loggt0  49570  elbigodm  49589  fllogbd  49594  rrx2xpref1o  49752  unilbss  49850  fdomne0  49882  f002  49886  xpco2  49889  imaf1homlem  50137  idemb  50189  uobeq2  50431  thincmo2  50456  thincmoALT  50459  fullthinc  50480  idfudiag1  50555  elsetrecslem  50714  dvsec  50778  dvcsc  50779  dvcot  50780  alseueu  50855