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  1548  eumo  2603  reurmo  3368  pssne  4026  pssn2lp  4032  ssnpss  4034  eldifn  4068  elinel2  4099  rabsnt  4691  eldifsni  4752  unimax  4904  ssintub  4925  moop2  5473  pwssun  5542  weso  5641  opelxp2  5693  predpo  6326  frpoinsg  6346  ordwe  6375  funmo  6554  funopg  6574  funun  6586  fununi  6615  funimaexg  6626  fndm  6642  frn  6717  f1ss  6785  f1ssr  6786  forn  6799  f1f1orn  6836  f1orescnv  6840  f1imacnv  6841  funcocnv2  6850  dffv2  6980  exfo  7105  foelrn  7107  foelrnf  7108  isorel  7334  isoini2  7347  f1ofveu  7414  fovcld  7547  onminesb  7807  onminsb  7808  tfisg  7865  tfis  7866  limomss  7882  nnlim  7891  ssnlim  7897  resf1ext2b  7947  curry1  8115  curry2  8118  f1o2ndf1  8133  fnwelem  8143  mpoxopn0yelv  8231  tz7.48lem  8451  tz7.48lemOLD  8452  dif20el  8514  oeordi  8597  oeeulem  8611  oeeui  8612  nnawordex  8647  swoer  8750  eceqoveq  8844  mapsnconst  8921  resixpfo  8965  boxcutc  8970  sdomnen  9009  en0  9046  en0ALT  9047  en0r  9048  en1  9052  dom0  9125  fodomr  9148  dif1enlem  9176  unxpdomlem3  9250  fineqvlem  9258  infn0  9295  fodomfir  9320  f1opwfi  9346  fsuppcolem  9394  fsuppco  9395  mapfienlem1  9398  mapfienlem2  9399  supub  9452  suplub  9453  ordtypelem2  9514  ordtypelem3  9515  ordtypelem6  9518  ordtypelem7  9519  wemapso2lem  9547  wdom2d  9575  brwdom3  9577  ixpiunwdom  9585  inf3lem2  9631  inf3lem6  9635  oancom  9653  infdifsn  9659  cantnfp1lem3  9682  cantnflem3  9693  cantnflem4  9694  oef1o  9700  cnfcom3  9706  tctr  9740  frinsg  9756  tz9.12lem3  9797  hfelhf  9915  hfsshf  9916  hfun  9919  hfuni  9925  scottex  9934  scottexOLD  9935  cardid2  10035  infxpenlem  10093  acni3  10127  cardaleph  10169  iscard3  10173  dfac5lem4  10206  dfac5lem5  10207  kmlem1  10230  cofsmo  10348  fin4en1  10388  enfin2i  10400  fin23lem28  10419  fin23lem38  10428  isf32lem6  10437  enfin1ai  10463  hsmexlem2  10506  hsmexlem4  10508  domtriomlem  10521  axdc2lem  10527  axdc3lem2  10530  ac6num  10558  zorn2lem2  10576  brdom3  10608  alephval2  10658  alephreg  10668  pwcfsdom  10669  smobeth  10672  fpwwe2lem5  10721  fpwwe2lem12  10728  canthp1lem2  10739  pwfseqlem3  10746  hargch  10759  winalim2  10782  gchina  10785  inar1  10861  0npi  10968  mulclpi  10979  mulcanpi  10986  nlt1pi  10992  nqereu  11015  prcdnq  11079  prnmax  11081  ltresr2  11227  axrnegex  11248  axpre-sup  11255  0nn0m1nnn0  12754  eluz2gt1  13048  1nuz2  13052  zsupss  13065  rpgt0  13134  ixxss1  13495  ixxss2  13496  ixxss12  13497  lbioo  13508  ubioo  13509  iccss2  13549  iccssico2  13552  elfzuz3  13654  serge0  14200  expge0  14242  expge1  14243  expaddzlem  14249  hashrabsn1  14519  hashfun  14583  ccatf1  14737  cshinj  14963  relexpuzrel  15206  shftfn  15227  01sqrexlem6  15415  rlimss  15670  lo1dm  15687  o1dm  15698  rlimrege0  15747  fsumf1o  15890  fsumge0  15963  incexc2  16008  supcvg  16026  fprodf1o  16114  divalglem9  16572  bitsfzolem  16605  bitsf1  16617  gcdcllem1  16670  bezout  16717  nprm  16864  dvdsprm  16880  coprm  16888  dfphi2  16952  phimullem  16957  phisum  16969  expnprm  17081  prmreclem2  17096  prmreclem5  17099  1arith  17106  4sqlem18  17141  vdwnnlem3  17176  ramtlecl  17179  rami  17194  0ram  17199  ramub1lem1  17205  prmgaplem5  17234  acsfiel  17829  isacs1i  17832  catlid  17858  catrid  17859  fullfo  18090  fthf1  18095  fthoppc  18101  invfuc  18153  prslem  18472  oduprs  18475  posi  18492  tleile  18594  resspos  18604  resstos  18605  dlatmjdi  18698  pslem  18747  tsrlin  18760  cnvtsr  18763  tsrdir  18779  mndid  18934  mhmf  18985  mhmlin  18989  mhm0  18990  mndind  19025  grpinvex  19155  grplinv  19201  mulgz  19313  mulgdirlem  19316  mulgdir  19317  mulgass  19322  nsgbi  19368  nmzbi  19375  ghmf  19435  ghmlin  19436  conjnsg  19469  gimf1o  19478  gagrpid  19509  gaf  19510  gaass  19512  psgnunilem5  19709  odid  19753  odf1o2  19788  gexid  19796  sylow1lem4  19816  pj1id  19914  efgredeu  19967  ablcmn  20002  cmncom  20013  mulgdi  20041  torsubg  20069  cyggenod2  20100  cygctb  20107  ghmcyg  20111  dprdf1o  20249  ablfacrplem  20282  ablfaclem2  20303  ablfac2  20306  simpg2nsg  20313  fincygsubgodexd  20330  ogrpinv0le  20351  ogrpsub  20352  ogrpaddlt  20353  crngmgp  20468  rnghmmgmhm  20674  rhmmhm  20711  rhmghm  20715  rimf1o  20730  nzrnz  20766  0ringbas  20780  subrgss  20825  subrg1cl  20833  rnghmsubcsetclem1  20884  zrinitorngc  20895  zrtermorngc  20896  rhmsubcsetclem1  20913  ringcinv  20924  zrtermoringc  20928  rrgeq0i  20952  domneq0  20961  domnrrg  20965  drngunit  20986  isdrng4  20993  fldcrngd  20996  drngmgp  21000  drngid  21001  drngdomn  21004  issubdrg  21038  fldhmsubc  21043  fldsdrgfld  21056  cntzsdrg  21060  abvge0  21075  srngcnv  21105  orngsqr  21124  ornglmulle  21125  orngrmulle  21126  ofldtos  21131  ofldlt1  21133  suborng  21134  subofld  21135  lmhmlin  21311  lmimf1o  21339  lvecdrng  21381  lspsolvlem  21421  islbs3  21434  lbsextlem3  21439  2idlelbas  21559  2idlcpblrng  21566  prmidl0  21635  qsidomlem1  21637  zringunit  21773  prmirredlem  21779  irinitoringc  21786  znidomb  21868  cygzn  21877  ofldchr  21883  psgndiflemB  21907  pjf  22020  frlmsslsp  22103  frlmlbs  22104  f1lindf  22129  lindsenlbs  22158  assalem  22166  psrbaglefi  22235  psrbagleadd1  22237  mplelsfi  22303  mplsubrglem  22312  mplcoe1  22347  mplbas2  22352  opsrtoslem2  22366  mhpmulcl  22471  psdmul  22488  coe1mul2  22589  matunitlindflem1  22995  matunitlindflem2  22996  matunitlindf  22997  pmatcoe1fsupp  23020  toponuni  23233  tpsuni  23255  mretopd  23411  neips  23432  neiptoptop  23450  neiptopnei  23451  perflp  23473  perfi  23474  cnf  23565  cnpf  23566  cnpimaex  23575  cnima  23584  t0sep  23643  t1ficld  23646  hausnei  23647  pnrmcld  23661  cnrmi  23679  cmpcov  23708  tgcmp  23720  hauscmplem  23725  connclo  23734  1stcclb  23763  2ndcdisj  23776  llyi  23794  nllyi  23795  ptpjpre1  23891  ptpjcn  23931  ptpjopn  23932  ptclsg  23935  dfac14  23938  txdis1cn  23955  pthaus  23958  hauseqlcld  23966  txkgen  23972  xkococn  23980  txconn  24009  hmeocnvcn  24081  fbssfi  24157  filss  24173  uffixfr  24243  flimneiss  24286  flimelbas  24288  flimfnfcls  24348  alexsubb  24366  alexsubALT  24371  ptcmplem2  24373  ptcmplem3  24374  ptcmplem4  24375  tmdgsum2  24416  ghmcnp  24435  tgpt0  24439  qustgplem  24441  istdrg2  24498  vscacn  24506  tvctdrg  24513  uspreg  24593  ucncn  24604  neipcfilu  24615  cuspcvg  24620  psmetxrge0  24633  isxmet2d  24647  prdsxmetlem  24688  imasdsf1olem  24693  xmstopn  24771  mstopn  24772  stdbdxmet  24835  prdsxmslem2  24849  nrgabv  24981  nmvs  24996  nvclvec  25017  nmoge0  25041  nghmcl  25047  nmoi  25048  nghmghm  25054  nmhmlmhm  25069  nmhmnghm  25070  icccmp  25146  xrge0gsumle  25154  metds0  25171  metdstri  25172  metdsre  25174  metdseq0  25175  metdscnlem  25176  metnrmlem1a  25179  icopnfcnv  25264  xrhmeo  25268  pcoval1  25335  cvslvec  25447  cvsunit  25453  recvs  25468  cphreccllem  25500  cphsscph  25573  cmetcvg  25607  lmle  25623  cmscmet  25668  cmetcusp1  25675  hlcph  25686  minveclem4  25754  ivthlem3  25775  ovolmge0  25799  ovolicc1  25838  ovolicc2lem3  25841  ovolicc2lem5  25843  dyadmbl  25922  i1ff  25998  i1frn  25999  i1fima2  26001  itg2monolem1  26072  dvnres  26252  c1liplem1  26317  c1lip2  26319  dvge0  26327  lhop1lem  26334  itgsubstlem  26369  fta1glem2  26488  fta1b  26491  idomrootle  26492  plyf  26517  plypf1  26532  plyadd  26537  plymul  26538  coeeu  26545  dgrlem  26549  coeid  26558  elqaalem3  26645  preimaaa  26647  aareccl  26654  eff1olem  26877  relogf1o  26895  logdmn0  26969  logcnlem2  26972  logcnlem3  26973  efopnlem1  26985  efopnlem2  26986  logtayl2  26991  cxpcn3lem  27076  cxpcn3  27077  logbgcd1irr  27123  atandmneg  27235  atandmcj  27238  efiatan2  27246  cosatan  27250  cosatanne0  27251  dvatan  27264  areage0  27292  cxp2lim  27305  jensenlem2  27316  jensen  27317  eldmgm  27350  dmgmaddn0  27351  dmlogdmgm  27352  lgamgulmlem2  27358  lgamgulmlem3  27359  lgamgulmlem5  27361  lgambdd  27365  lgamucov  27366  ftalem3  27403  efnnfsumcl  27431  efchtdvds  27487  sqff1o  27510  fsumdvdsdiaglem  27511  dvdsppwf1o  27514  dvdsflf1o  27515  musum  27519  muinv  27521  mpodvdsmulf1o  27522  dvdsmulf1o  27524  lgsfle1  27634  lgsle1  27640  lgsdirprm  27659  lgsne0  27663  lgseisenlem3  27705  lgseisenlem4  27706  lgsquadlem1  27708  lgsquadlem2  27709  chebbnd1  27800  chtppilim  27803  chpchtlim  27807  chpo1ub  27808  dchrmusumlema  27821  dchrvmasumlem1  27823  dchrisum0lema  27842  dchrisum0lem2a  27845  logsqvma  27870  selberg3lem2  27886  pntrsumo1  27893  pnt2  27941  ostthlem1  27955  ostth3  27966  ltsval2  28014  leftlt  28240  rightgt  28241  precsexlem8  28601  precsexlem9  28602  precsexlem11  28604  elons2  28645  onleft  28647  ltonold  28648  oncutleft  28650  oncutlt  28651  zcuts0  28795  axtgcgrrflx  28925  axtgcgrid  28926  axtgsegcon  28927  axtg5seg  28928  axtgbtwnid  28929  axtgpasch  28930  axtgcont1  28931  tglng  29010  axcontlem7  29549  axcontlem10  29552  upgrle  29669  umgredg2  29679  lfgredgge2  29703  usgredg2ALT  29775  usgr1vr  29837  usgrexmpledg  29844  upgrres1  29895  fusgrvtxfi  29901  vtxnbuvtx  29973  cusgrcplgr  30002  vdumgr0  30062  vtxdgoddnumeven  30135  trlres  30284  pthhashvtx  30316  usgr2pth  30351  cyclispthon  30394  clwwlknlen  30624  clwwnonrepclwwnon  30947  2clwwlk2  30950  ablocom  31151  phpar2  31426  cbncms  31468  hlph  31492  hcaucvg  31789  hlimconvi  31794  shaddcl  31820  shmulcl  31821  chlimi  31837  chcompl  31845  choc1  31930  nmopre  32473  cnopc  32516  lnopl  32517  unop  32518  hmop  32525  cnfnc  32533  lnfnl  32534  nlelshi  32663  cnlnadjlem5  32674  elpjidm  32787  mdslle1i  32920  mdslle2i  32921  atcv0  32945  aciunf1lem  33299  padct  33353  ssnnssfz  33422  swrdrndisj  33561  ressprs  33570  pwrssmgc  33604  wrdpmtrlast  33697  cyc3evpm  33754  cycpmgcl  33757  cycpmconjslem2  33759  cyc3conja  33761  isarchi3  33791  archirng  33792  archirngz  33793  archiabllem1a  33795  archiabllem1b  33796  archiabllem2a  33798  archiabllem2c  33799  archiabllem2b  33800  archiabl  33802  isarchiofld  33803  elrgspnlem1  33846  elrgspnlem2  33847  elrgspnlem4  33849  elrgspnsubrun  33853  ricnzr1  33892  ricdomn1  33893  nn0omnd  33948  quslsm  33999  nsgmgclem  34005  nsgmgc  34006  mxidlirred  34040  krull  34046  ufdprmidl  34116  1arithufdlem4  34122  extvfvcl  34211  mplvrpmga  34220  sradrng  34257  extdg1id  34341  ply1annnr  34378  madjusmdetlem4  34505  qtophaus  34511  crefi  34522  cmpcref  34525  cmppcmp  34533  pcmplfin  34535  zart0  34554  tpr2rico  34587  rge0scvg  34624  zrhunitpreima  34651  qqhrhm  34664  esummono  34729  gsumesum  34734  esumrnmpt2  34743  esumpinfval  34748  esumpcvgval  34753  esumpmono  34754  0elsiga  34789  sigaclcu  34792  issgon  34798  inelpisys  34830  ldsysgenld  34836  ldgenpisyslem1  34839  sxuni  34869  isrnmeas  34876  measvuni  34890  measssd  34891  ddemeas  34912  imambfm  34937  elmbfmvol2  34942  dya2icoseg2  34953  omssubaddlem  34974  omssubadd  34975  carsgsigalem  34990  pmeasmono  34999  sibfinima  35014  oddpwdc  35029  oddpwdcv  35030  eulerpartlemf  35045  eulerpartlemt  35046  eulerpartlemr  35049  eulerpartlemgvv  35051  eulerpartlemgs2  35055  fiblem  35073  probtot  35087  ballotlem4  35174  ballotlem5  35175  ballotlemfrc  35202  ballotlemirc  35207  ballotth  35213  hgt750lemb  35328  bnj642  35422  bnj643  35423  bnj645  35424  bnj707  35429  bnj1379  35503  bnj1538  35528  bnj110  35531  bnj93  35536  bnj906  35603  bnj1006  35633  bnj1110  35655  bnj1121  35658  bnj1204  35685  bnj1321  35700  bnj1364  35701  bnj1398  35707  bnj1450  35723  bnj1312  35731  bnj1501  35740  bnj1523  35744  f1preimaex  35756  soinfdom  35761  elscottrank  35792  elscottrankss  35794  tz9.1regs  35851  onprcf1acwevdlem2  35958  onvfowev  35962  onprcf1of1ord  35967  subfacp1lem3  36016  subfacp1lem5  36018  pconncn  36058  connpconn  36069  cvmcov  36097  cvmliftlem1  36119  cvmliftlem10  36128  cvmlift2lem11  36147  cvmlift2lem12  36148  msubff1  36390  mvhf1  36393  mthmpps  36416  mclspps  36418  fundmpss  36607  funpartfun  36782  fnetg  37208  neibastop1  37222  filnetlem3  37243  onint1  37312  weiunlem  37326  weiunpo  37328  weiunse  37331  bj-nnfa  37705  bj-idres  38157  bj-rvecrr  38294  icorempo  38350  pibt2  38416  wl-nfeqfb  38544  phpreu  38603  fin2solem  38605  fin2so  38606  ptrest  38613  poimirlem1  38615  poimirlem2  38616  poimirlem3  38617  poimirlem4  38618  poimirlem5  38619  poimirlem6  38620  poimirlem7  38621  poimirlem8  38622  poimirlem9  38623  poimirlem10  38624  poimirlem11  38625  poimirlem12  38626  poimirlem13  38627  poimirlem14  38628  poimirlem15  38629  poimirlem16  38630  poimirlem17  38631  poimirlem18  38632  poimirlem19  38633  poimirlem20  38634  poimirlem21  38635  poimirlem22  38636  poimirlem23  38637  poimirlem24  38638  poimirlem26  38640  poimirlem27  38641  poimirlem29  38643  poimirlem31  38645  mblfinlem2  38652  dvtan  38664  itg2gt0cn  38669  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  cover2  38725  indexa  38743  istotbnd3  38781  sstotbnd2  38784  sstotbnd  38785  totbndss  38787  equivtotbnd  38788  isbnd3  38794  totbndbnd  38799  equivbnd  38800  prdsbnd  38803  prdstotbnd  38804  heibor  38831  zrdivrng  38963  crngocom  39011  isfld2  39015  dmncrng  39066  eqvrelrel  39689  disjrel  39838  disjdmqscossss  39914  prter2  40014  toycom  40106  lsateln0  40128  lpssat  40146  lssat  40149  oposlem  40315  olop  40347  omllaw  40376  cvlexch1  40461  dihpN  42469  mapdordlem2  42770  linvh  43222  idomnnzpownz  43258  idomnnzgmulnz  43259  aks6d1c5lem2  43264  deg1pow  43267  redvmptabs  43487  readvrec2  43488  readvrec  43489  mhphflem  43700  prjspertr  43709  nacsfg  43792  nacsfix  43799  mzpindd  43833  diophrw  43846  diophrex  43862  rexzrexnn0  43887  pell1234qrdich  43944  rmspecnonsq  43990  rmspecfund  43992  rmspecpos  43999  monotoddzzfi  44025  ltrmxnn0  44032  rmxnn  44034  jm2.23  44079  jm3.1lem2  44101  dnnumch3  44130  lnmlssfg  44158  lnmlmic  44166  lnrlnm  44191  lnr2i  44194  lpirlnr  44195  hbtlem6  44207  hbt  44208  mnccoe  44216  proot1mul  44272  proot1hash  44273  deg1mhm  44278  ondif1i  44340  limnsuc  44343  cantnfresb  44402  succlg  44406  ntrneifv2  45156  grucollcld  45320  mnurndlem1  45341  ismnushort  45361  radcnvrat  45374  binomcxplemdvbinom  45413  binomcxplemcvg  45414  binomcxplemnotnn0  45416  ordelordALT  45596  2uasbanh  45620  ordelordALTVD  45925  relprel  46017  elixpconstg  46180  rabidim2  46193  disjinfi  46283  supminfxr2  46555  sumnnodd  46718  stoweidlem7  47093  stoweidlem14  47100  stoweidlem16  47102  stoweidlem24  47110  stoweidlem31  47117  stoweidlem54  47140  wallispilem3  47153  fourierdlem42  47235  fourierdlem48  47240  fourierdlem51  47243  fourierdlem64  47256  fourierdlem76  47268  fourierdlem79  47271  fourierdlem81  47273  fourierdlem87  47279  etransclem28  47348  etransclem32  47352  sge0fodjrnlem  47502  hoidmvlelem3  47683  ovolval5lem3  47740  pimrecltpos  47794  pimrecltneg  47810  issmflem  47813  smfaddlem1  47849  smfsuplem1  47897  smfsuplem3  47899  smflimsuplem7  47912  smfliminflem  47916  chndin  47977  chnrin  47982  nfunsnafv  48288  faovcl  48346  tz6.12-2-afv2  48383  tz6.12i-afv2  48389  sprel  48642  evendiv2z  48806  oddp1div2z  48807  2dvdseven  48827  2ndvdsodd  48829  perfectALTVlem1  48895  sbgoldbm  48958  upgrimtrls  49080  upgrimpthslem1  49081  upgrimspths  49084  upgrimcycls  49085  uhgrimisgrgric  49105  gpgprismgr4cycllem2  49270  clintopcllaw  49384  uzlidlring  49408  rngccatidALTV  49445  funcringcsetcALTV2lem7  49469  ringccatidALTV  49479  ringcinvALTV  49483  funcringcsetclem7ALTV  49492  fldhmsubcALTV  49506  ssnn0ssfz  49537  el0ldepsnzr  49655  regt1loggt0  49724  elbigodm  49743  fllogbd  49748  rrx2xpref1o  49906  unilbss  50004  fdomne0  50036  f002  50040  xpco2  50043  imaf1homlem  50291  idemb  50343  uobeq2  50585  thincmo2  50610  thincmoALT  50613  fullthinc  50634  idfudiag1  50709  elsetrecslem  50868  dvsec  50932  dvcsc  50933  dvcot  50934  alseueu  51009