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  2572  reurmo  3347  pssne  4047  pssn2lp  4052  ssnpss  4054  eldifn  4080  elinel2  4150  rabsnt  4682  eldifsni  4740  unimax  4893  ssintub  4914  moop2  5440  pwssun  5506  weso  5605  opelxp2  5657  predpo  6266  frpoinsg  6286  ordwe  6315  funmo  6493  funopg  6511  funun  6523  fununi  6552  funimaexg  6564  fndm  6580  frn  6654  f1ss  6720  f1ssr  6721  forn  6734  f1f1orn  6770  f1orescnv  6774  f1imacnv  6775  funcocnv2  6784  dffv2  6912  exfo  7033  foelrn  7035  foelrnf  7036  isorel  7255  isoini2  7268  f1ofveu  7335  fovcld  7468  onminesb  7721  onminsb  7722  tfisg  7779  tfis  7780  limomss  7796  nnlim  7805  ssnlim  7811  resf1ext2b  7860  curry1  8029  curry2  8032  f1o2ndf1  8047  fnwelem  8056  mpoxopn0yelv  8138  tz7.48lem  8355  dif20el  8415  oeordi  8497  oeeulem  8511  oeeui  8512  nnawordex  8547  swoer  8648  eceqoveq  8741  mapsnconst  8811  resixpfo  8855  boxcutc  8860  sdomnen  8898  en0  8935  en0ALT  8936  en0r  8937  en1  8941  dom0  9013  fodomr  9036  dif1enlem  9064  unxpdomlem3  9137  fineqvlem  9145  infn0  9181  fodomfir  9207  f1opwfi  9235  fsuppcolem  9280  fsuppco  9281  mapfienlem1  9284  mapfienlem2  9285  supub  9338  suplub  9339  ordtypelem2  9400  ordtypelem3  9401  ordtypelem6  9404  ordtypelem7  9405  wemapso2lem  9433  wdom2d  9461  brwdom3  9463  ixpiunwdom  9471  inf3lem2  9514  inf3lem6  9518  oancom  9536  infdifsn  9542  cantnfp1lem3  9565  cantnflem3  9576  cantnflem4  9577  oef1o  9583  cnfcom3  9589  tctr  9625  frinsg  9636  tz9.12lem3  9674  scottex  9770  cardid2  9838  infxpenlem  9896  acni3  9930  cardaleph  9972  iscard3  9976  dfac5lem4  10009  dfac5lem5  10010  dfac5lem4OLD  10011  kmlem1  10034  cofsmo  10152  fin4en1  10192  enfin2i  10204  fin23lem28  10223  fin23lem38  10232  isf32lem6  10241  enfin1ai  10267  hsmexlem2  10310  hsmexlem4  10312  domtriomlem  10325  axdc2lem  10331  axdc3lem2  10334  ac6num  10362  zorn2lem2  10380  brdom3  10411  alephval2  10455  alephreg  10465  pwcfsdom  10466  smobeth  10469  fpwwe2lem5  10518  fpwwe2lem12  10525  canthp1lem2  10536  pwfseqlem3  10543  hargch  10556  winalim2  10579  gchina  10582  inar1  10658  0npi  10765  mulclpi  10776  mulcanpi  10783  nlt1pi  10789  nqereu  10812  prcdnq  10876  prnmax  10878  ltresr2  11024  axrnegex  11045  axpre-sup  11052  eluz2gt1  12810  1nuz2  12814  zsupss  12827  rpgt0  12895  ixxss1  13255  ixxss2  13256  ixxss12  13257  lbioo  13268  ubioo  13269  iccss2  13309  iccssico2  13312  elfzuz3  13413  serge0  13955  expge0  13997  expge1  13998  expaddzlem  14004  hashrabsn1  14273  hashfun  14336  cshinj  14710  relexpuzrel  14951  shftfn  14972  01sqrexlem6  15146  rlimss  15401  lo1dm  15418  o1dm  15429  rlimrege0  15478  fsumf1o  15622  fsumge0  15694  incexc2  15737  supcvg  15755  fprodf1o  15845  divalglem9  16304  bitsfzolem  16337  bitsf1  16349  gcdcllem1  16402  bezout  16446  nprm  16591  dvdsprm  16606  coprm  16614  dfphi2  16677  phimullem  16682  phisum  16694  expnprm  16806  prmreclem2  16821  prmreclem5  16824  1arith  16831  4sqlem18  16866  vdwnnlem3  16901  ramtlecl  16904  rami  16919  0ram  16924  ramub1lem1  16930  prmgaplem5  16959  acsfiel  17552  isacs1i  17555  catlid  17581  catrid  17582  fullfo  17813  fthf1  17818  fthoppc  17824  invfuc  17876  prslem  18195  oduprs  18198  posi  18215  tleile  18317  resspos  18327  resstos  18328  dlatmjdi  18421  pslem  18470  tsrlin  18483  cnvtsr  18486  tsrdir  18502  mndid  18644  mhmf  18689  mhmlin  18693  mhm0  18694  mndind  18728  grpinvex  18848  grplinv  18894  mulgz  19007  mulgdirlem  19010  mulgdir  19011  mulgass  19016  nsgbi  19062  nmzbi  19069  ghmf  19125  ghmlin  19126  conjnsg  19159  gimf1o  19168  gagrpid  19199  gaf  19200  gaass  19202  psgnunilem5  19399  odid  19443  odf1o2  19478  gexid  19486  sylow1lem4  19506  pj1id  19604  efgredeu  19657  ablcmn  19692  cmncom  19703  mulgdi  19731  torsubg  19759  cyggenod2  19790  cygctb  19797  ghmcyg  19801  dprdf1o  19939  ablfacrplem  19972  ablfaclem2  19993  ablfac2  19996  simpg2nsg  20003  fincygsubgodexd  20020  ogrpinv0le  20041  ogrpsub  20042  ogrpaddlt  20043  crngmgp  20152  rnghmmgmhm  20354  rhmmhm  20390  rhmghm  20394  rimf1o  20403  nzrnz  20423  0ringbas  20436  subrgss  20480  subrg1cl  20488  rnghmsubcsetclem1  20539  zrinitorngc  20550  zrtermorngc  20551  rhmsubcsetclem1  20568  ringcinv  20579  zrtermoringc  20583  rrgeq0i  20607  domneq0  20616  domnrrg  20621  drngunit  20642  fldcrngd  20650  drngmgp  20653  drngid  20654  drngdomn  20657  issubdrg  20688  fldhmsubc  20693  fldsdrgfld  20706  cntzsdrg  20710  abvge0  20725  srngcnv  20755  orngsqr  20774  ornglmulle  20775  orngrmulle  20776  ofldtos  20781  ofldlt1  20783  suborng  20784  subofld  20785  lmhmlin  20962  lmimf1o  20990  lvecdrng  21032  lspsolvlem  21072  islbs3  21085  lbsextlem3  21090  2idlelbas  21194  2idlcpblrng  21201  zringunit  21396  prmirredlem  21402  irinitoringc  21409  znidomb  21491  cygzn  21500  ofldchr  21506  psgndiflemB  21530  pjf  21643  frlmsslsp  21726  frlmlbs  21727  f1lindf  21752  assalem  21787  psrbaglefi  21856  psrbagleadd1  21858  mplelsfi  21925  mplsubrglem  21934  mplcoe1  21965  mplbas2  21970  opsrtoslem2  21984  mhpmulcl  22057  psdmul  22074  coe1mul2  22176  pmatcoe1fsupp  22609  toponuni  22822  tpsuni  22844  mretopd  23000  neips  23021  neiptoptop  23039  neiptopnei  23040  perflp  23062  perfi  23063  cnf  23154  cnpf  23155  cnpimaex  23164  cnima  23173  t0sep  23232  t1ficld  23235  hausnei  23236  pnrmcld  23250  cnrmi  23268  cmpcov  23297  tgcmp  23309  hauscmplem  23314  connclo  23323  1stcclb  23352  2ndcdisj  23364  llyi  23382  nllyi  23383  ptpjpre1  23479  ptpjcn  23519  ptpjopn  23520  ptclsg  23523  dfac14  23526  txdis1cn  23543  pthaus  23546  hauseqlcld  23554  txkgen  23560  xkococn  23568  txconn  23597  hmeocnvcn  23669  fbssfi  23745  filss  23761  uffixfr  23831  flimneiss  23874  flimelbas  23876  flimfnfcls  23936  alexsubb  23954  alexsubALT  23959  ptcmplem2  23961  ptcmplem3  23962  ptcmplem4  23963  tmdgsum2  24004  ghmcnp  24023  tgpt0  24027  qustgplem  24029  istdrg2  24086  vscacn  24094  tvctdrg  24101  uspreg  24181  ucncn  24192  neipcfilu  24203  cuspcvg  24208  psmetxrge0  24221  isxmet2d  24235  prdsxmetlem  24276  imasdsf1olem  24281  xmstopn  24359  mstopn  24360  stdbdxmet  24423  prdsxmslem2  24437  nrgabv  24569  nmvs  24584  nvclvec  24605  nmoge0  24629  nghmcl  24635  nmoi  24636  nghmghm  24642  nmhmlmhm  24657  nmhmnghm  24658  icccmp  24734  xrge0gsumle  24742  metds0  24759  metdstri  24760  metdsre  24762  metdseq0  24763  metdscnlem  24764  metnrmlem1a  24767  icopnfcnv  24860  xrhmeo  24864  pcoval1  24933  cvslvec  25045  cvsunit  25051  recvs  25066  cphreccllem  25098  cphsscph  25171  cmetcvg  25205  lmle  25221  cmscmet  25266  cmetcusp1  25273  hlcph  25284  minveclem4  25352  ivthlem3  25374  ovolmge0  25398  ovolicc1  25437  ovolicc2lem3  25440  ovolicc2lem5  25442  dyadmbl  25521  i1ff  25597  i1frn  25598  i1fima2  25600  itg2monolem1  25671  dvnres  25853  c1liplem1  25921  c1lip2  25923  dvge0  25931  lhop1lem  25938  itgsubstlem  25975  fta1glem2  26094  fta1b  26097  idomrootle  26098  plyf  26123  plypf1  26137  plyadd  26142  plymul  26143  coeeu  26150  dgrlem  26154  coeid  26163  elqaalem3  26249  aareccl  26254  eff1olem  26477  relogf1o  26495  logdmn0  26569  logcnlem2  26572  logcnlem3  26573  efopnlem1  26585  efopnlem2  26586  logtayl2  26591  cxpcn3lem  26677  cxpcn3  26678  logbgcd1irr  26724  atandmneg  26836  atandmcj  26839  efiatan2  26847  cosatan  26851  cosatanne0  26852  dvatan  26865  areage0  26893  cxp2lim  26907  jensenlem2  26918  jensen  26919  eldmgm  26952  dmgmaddn0  26953  dmlogdmgm  26954  lgamgulmlem2  26960  lgamgulmlem3  26961  lgamgulmlem5  26963  lgambdd  26967  lgamucov  26968  ftalem3  27005  efnnfsumcl  27033  efchtdvds  27089  sqff1o  27112  fsumdvdsdiaglem  27113  dvdsppwf1o  27116  dvdsflf1o  27117  musum  27121  muinv  27123  mpodvdsmulf1o  27124  dvdsmulf1o  27126  lgsfle1  27237  lgsle1  27243  lgsdirprm  27262  lgsne0  27266  lgseisenlem3  27308  lgseisenlem4  27309  lgsquadlem1  27311  lgsquadlem2  27312  chebbnd1  27403  chtppilim  27406  chpchtlim  27410  chpo1ub  27411  dchrmusumlema  27424  dchrvmasumlem1  27426  dchrisum0lema  27445  dchrisum0lem2a  27448  logsqvma  27473  selberg3lem2  27489  pntrsumo1  27496  pnt2  27544  ostthlem1  27558  ostth3  27569  sltval2  27588  leftlt  27801  rightgt  27802  precsexlem8  28145  precsexlem9  28146  precsexlem11  28148  elons2  28188  onsleft  28190  sltonold  28191  onscutleft  28193  onscutlt  28194  axtgcgrrflx  28433  axtgcgrid  28434  axtgsegcon  28435  axtg5seg  28436  axtgbtwnid  28437  axtgpasch  28438  axtgcont1  28439  tglng  28517  axcontlem7  28941  axcontlem10  28944  upgrle  29061  umgredg2  29071  lfgredgge2  29095  usgredg2ALT  29164  usgr1vr  29226  usgrexmpledg  29233  upgrres1  29284  fusgrvtxfi  29290  vtxnbuvtx  29362  cusgrcplgr  29391  vdumgr0  29452  vtxdgoddnumeven  29525  trlres  29670  usgr2pth  29735  cyclispthon  29775  clwwlknlen  30002  clwwnonrepclwwnon  30315  2clwwlk2  30318  ablocom  30518  phpar2  30793  cbncms  30835  hlph  30859  hcaucvg  31156  hlimconvi  31161  shaddcl  31187  shmulcl  31188  chlimi  31204  chcompl  31212  choc1  31297  nmopre  31840  cnopc  31883  lnopl  31884  unop  31885  hmop  31892  cnfnc  31900  lnfnl  31901  nlelshi  32030  cnlnadjlem5  32041  elpjidm  32154  mdslle1i  32287  mdslle2i  32288  atcv0  32312  chpssati  32333  aciunf1lem  32634  padct  32691  ssnnssfz  32760  ccatf1  32920  swrdrndisj  32928  ressprs  32937  pwrssmgc  32971  wrdpmtrlast  33052  cyc3evpm  33109  cycpmgcl  33112  cycpmconjslem2  33114  cyc3conja  33116  isarchi3  33146  archirng  33147  archirngz  33148  archiabllem1a  33150  archiabllem1b  33151  archiabllem2a  33153  archiabllem2c  33154  archiabllem2b  33155  archiabl  33157  isarchiofld  33158  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnlem4  33202  elrgspnsubrun  33206  isdrng4  33251  nn0omnd  33299  quslsm  33360  nsgmgclem  33366  nsgmgc  33367  prmidl0  33405  qsidomlem1  33407  mxidlirred  33427  krull  33434  ufdprmidl  33496  1arithufdlem4  33502  mplvrpmlem  33563  mplvrpmga  33565  sradrng  33584  extdg1id  33669  ply1annnr  33706  madjusmdetlem4  33833  qtophaus  33839  crefi  33850  cmpcref  33853  cmppcmp  33861  pcmplfin  33863  zart0  33882  tpr2rico  33915  rge0scvg  33952  zrhunitpreima  33979  qqhrhm  33992  esummono  34057  gsumesum  34062  esumrnmpt2  34071  esumpinfval  34076  esumpcvgval  34081  esumpmono  34082  0elsiga  34117  sigaclcu  34120  issgon  34126  inelpisys  34157  ldsysgenld  34163  ldgenpisyslem1  34166  sxuni  34196  isrnmeas  34203  measvuni  34217  measssd  34218  ddemeas  34239  imambfm  34265  elmbfmvol2  34270  dya2icoseg2  34281  omssubaddlem  34302  omssubadd  34303  carsgsigalem  34318  pmeasmono  34327  sibfinima  34342  oddpwdc  34357  oddpwdcv  34358  eulerpartlemf  34373  eulerpartlemt  34374  eulerpartlemr  34377  eulerpartlemgvv  34379  eulerpartlemgs2  34383  fiblem  34401  probtot  34415  ballotlem4  34502  ballotlem5  34503  ballotlemfrc  34530  ballotlemirc  34535  ballotth  34541  hgt750lemb  34659  bnj642  34750  bnj643  34751  bnj645  34752  bnj707  34757  bnj1379  34832  bnj1538  34857  bnj110  34860  bnj93  34865  bnj906  34932  bnj1006  34962  bnj1110  34984  bnj1121  34987  bnj1204  35014  bnj1321  35029  bnj1364  35030  bnj1398  35036  bnj1450  35052  bnj1312  35060  bnj1501  35069  bnj1523  35073  tz9.1regs  35102  0nn0m1nnn0  35125  subfacp1lem3  35194  subfacp1lem5  35196  pconncn  35236  connpconn  35247  cvmcov  35275  cvmliftlem1  35297  cvmliftlem10  35306  cvmlift2lem11  35325  cvmlift2lem12  35326  msubff1  35568  mvhf1  35571  mthmpps  35594  mclspps  35596  fundmpss  35779  funpartfun  35956  fnetg  36358  neibastop1  36372  filnetlem3  36393  onint1  36462  weiunlem2  36476  weiunpo  36478  weiunse  36481  bj-nnfa  36741  bj-idres  37173  bj-rvecrr  37310  icorempo  37364  pibt2  37430  wl-nfeqfb  37549  phpreu  37623  fin2solem  37625  fin2so  37626  lindsenlbs  37634  matunitlindflem1  37635  matunitlindflem2  37636  matunitlindf  37637  ptrest  37638  poimirlem1  37640  poimirlem2  37641  poimirlem3  37642  poimirlem4  37643  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem9  37648  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem13  37652  poimirlem14  37653  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem18  37657  poimirlem19  37658  poimirlem20  37659  poimirlem21  37660  poimirlem22  37661  poimirlem23  37662  poimirlem24  37663  poimirlem26  37665  poimirlem27  37666  poimirlem29  37668  poimirlem31  37670  mblfinlem2  37677  dvtan  37689  itg2gt0cn  37694  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  cover2  37734  indexa  37752  istotbnd3  37790  sstotbnd2  37793  sstotbnd  37794  totbndss  37796  equivtotbnd  37797  isbnd3  37803  totbndbnd  37808  equivbnd  37809  prdsbnd  37812  prdstotbnd  37813  heibor  37840  zrdivrng  37972  crngocom  38020  isfld2  38024  dmncrng  38075  eqvrelrel  38613  disjrel  38747  disjdmqscossss  38820  prter2  38899  toycom  38991  lsateln0  39013  lpssat  39031  lssat  39034  oposlem  39200  olop  39232  omllaw  39261  cvlexch1  39346  dihpN  41354  mapdordlem2  41655  linvh  42108  idomnnzpownz  42144  idomnnzgmulnz  42145  aks6d1c5lem2  42150  deg1pow  42153  redvmptabs  42372  readvrec2  42373  readvrec  42374  mhphflem  42608  prjspertr  42617  nacsfg  42717  nacsfix  42724  mzpindd  42758  diophrw  42771  diophrex  42787  rexzrexnn0  42816  pell1234qrdich  42873  rmspecnonsq  42919  rmspecfund  42921  rmspecpos  42928  monotoddzzfi  42954  ltrmxnn0  42961  rmxnn  42963  jm2.23  43008  jm3.1lem2  43030  dnnumch3  43059  lnmlssfg  43092  lnmlmic  43100  lnrlnm  43125  lnr2i  43128  lpirlnr  43129  hbtlem6  43141  hbt  43142  mnccoe  43150  proot1mul  43206  proot1hash  43207  deg1mhm  43212  ondif1i  43274  limnsuc  43277  cantnfresb  43336  succlg  43340  ntrneifv2  44092  grucollcld  44272  mnurndlem1  44293  ismnushort  44313  radcnvrat  44326  binomcxplemdvbinom  44365  binomcxplemcvg  44366  binomcxplemnotnn0  44368  ordelordALT  44549  2uasbanh  44573  ordelordALTVD  44878  relprel  44963  elixpconstg  45105  rabidim2  45118  disjinfi  45208  supminfxr2  45486  sumnnodd  45649  stoweidlem7  46024  stoweidlem14  46031  stoweidlem16  46033  stoweidlem24  46041  stoweidlem31  46048  stoweidlem54  46071  wallispilem3  46084  fourierdlem42  46166  fourierdlem48  46171  fourierdlem51  46174  fourierdlem64  46187  fourierdlem76  46199  fourierdlem79  46202  fourierdlem81  46204  fourierdlem87  46210  etransclem28  46279  etransclem32  46283  sge0fodjrnlem  46433  hoidmvlelem3  46614  ovolval5lem3  46671  pimrecltpos  46725  pimrecltneg  46741  issmflem  46744  smfaddlem1  46780  smfsuplem1  46828  smfsuplem3  46830  smflimsuplem7  46843  smfliminflem  46847  nfunsnafv  47152  faovcl  47210  tz6.12-2-afv2  47247  tz6.12i-afv2  47253  sprel  47494  evendiv2z  47642  oddp1div2z  47643  2dvdseven  47663  2ndvdsodd  47665  perfectALTVlem1  47731  sbgoldbm  47794  upgrimtrls  47916  upgrimpthslem1  47917  upgrimspths  47920  upgrimcycls  47921  uhgrimisgrgric  47941  gpgprismgr4cycllem2  48106  clintopcllaw  48221  uzlidlring  48245  rngccatidALTV  48282  funcringcsetcALTV2lem7  48306  ringccatidALTV  48316  ringcinvALTV  48320  funcringcsetclem7ALTV  48329  fldhmsubcALTV  48343  ssnn0ssfz  48359  el0ldepsnzr  48478  regt1loggt0  48547  elbigodm  48566  fllogbd  48571  rrx2xpref1o  48729  unilbss  48828  fdomne0  48860  f002  48864  xpco2  48867  imaf1homlem  49118  idemb  49170  uobeq2  49412  thincmo2  49437  thincmoALT  49440  fullthinc  49461  idfudiag1  49536  elsetrecslem  49710