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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 495	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  simplbiim  504  xornan  1512  eumo  2578  reurmo  3354  pssne  4027  pssn2lp  4032  ssnpss  4034  eldifn  4058  elinel2  4126  rabsnt  4664  eldifsni  4720  unimax  4874  ssintub  4894  moop2  5410  pwssun  5476  weso  5571  opelxp2  5622  predpo  6215  frpoinsg  6231  wfisgOLD  6242  ordwe  6264  funmo  6434  funopg  6452  funun  6464  fununi  6493  fndm  6520  frn  6591  f1ss  6660  f1ssr  6661  forn  6675  f1f1orn  6711  f1orescnv  6715  f1imacnv  6716  funcocnv2  6724  dffv2  6845  exfo  6963  foelrn  6964  isorel  7177  isoini2  7190  f1ofveu  7250  fovcl  7380  onminesb  7620  onminsb  7621  tfis  7676  limomss  7692  nnlim  7701  ssnlim  7707  curry1  7915  curry2  7918  f1o2ndf1  7934  fnwelem  7943  mpoxopn0yelv  8000  wfrlem5OLD  8115  tz7.48lem  8242  dif20el  8297  oeordi  8380  oeeulem  8394  oeeui  8395  nnawordex  8430  swoer  8486  eceqoveq  8569  mapsnconst  8638  resixpfo  8682  boxcutc  8687  sdomnen  8724  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  fodomr  8864  dif1enlem  8905  unxpdomlem3  8958  fineqvlem  8966  f1opwfi  9053  fsuppcolem  9090  fsuppco  9091  mapfienlem1  9094  mapfienlem2  9095  supub  9148  suplub  9149  ordtypelem2  9208  ordtypelem3  9209  ordtypelem6  9212  ordtypelem7  9213  wemapso2lem  9241  wdom2d  9269  brwdom3  9271  ixpiunwdom  9279  inf3lem2  9317  inf3lem6  9321  oancom  9339  infdifsn  9345  cantnfp1lem3  9368  cantnflem3  9379  cantnflem4  9380  oef1o  9386  cnfcom3  9392  tctr  9429  frinsg  9440  tz9.12lem3  9478  scottex  9574  cardid2  9642  infxpenlem  9700  acni3  9734  cardaleph  9776  iscard3  9780  dfac5lem4  9813  dfac5lem5  9814  kmlem1  9837  cofsmo  9956  fin4en1  9996  enfin2i  10008  fin23lem28  10027  fin23lem38  10036  isf32lem6  10045  enfin1ai  10071  hsmexlem2  10114  hsmexlem4  10116  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  ac6num  10166  zorn2lem2  10184  brdom3  10215  alephval2  10259  alephreg  10269  pwcfsdom  10270  smobeth  10273  fpwwe2lem5  10322  fpwwe2lem12  10329  canthp1lem2  10340  pwfseqlem3  10347  hargch  10360  winalim2  10383  gchina  10386  inar1  10462  0npi  10569  mulclpi  10580  mulcanpi  10587  nlt1pi  10593  nqereu  10616  prcdnq  10680  prnmax  10682  ltresr2  10828  axrnegex  10849  axpre-sup  10856  eluz2gt1  12589  1nuz2  12593  zsupss  12606  rpgt0  12671  ixxss1  13026  ixxss2  13027  ixxss12  13028  lbioo  13039  ubioo  13040  iccss2  13079  iccssico2  13082  elfzuz3  13182  serge0  13705  expge0  13747  expge1  13748  expaddzlem  13754  hashrabsn1  14017  hashfun  14080  cshinj  14452  relexpuzrel  14691  shftfn  14712  sqrlem6  14887  rlimss  15139  lo1dm  15156  o1dm  15167  rlimrege0  15216  fsumf1o  15363  fsumge0  15435  incexc2  15478  supcvg  15496  fprodf1o  15584  divalglem9  16038  bitsfzolem  16069  bitsf1  16081  gcdcllem1  16134  bezout  16179  nprm  16321  dvdsprm  16336  coprm  16344  dfphi2  16403  phimullem  16408  phisum  16419  expnprm  16531  prmreclem2  16546  prmreclem5  16549  1arith  16556  4sqlem18  16591  vdwnnlem3  16626  ramtlecl  16629  rami  16644  0ram  16649  ramub1lem1  16655  prmgaplem5  16684  acsfiel  17280  isacs1i  17283  catlid  17309  catrid  17310  fullfo  17544  fthf1  17549  fthoppc  17555  invfuc  17608  prslem  17931  posi  17950  tleile  18054  dlatmjdi  18156  pslem  18205  tsrlin  18218  cnvtsr  18221  tsrdir  18237  mndid  18310  mhmf  18350  mhmlin  18352  mhm0  18353  mndind  18381  grpinvex  18502  grplinv  18543  mulgz  18646  mulgdirlem  18649  mulgdir  18650  mulgass  18655  nsgbi  18700  nmzbi  18707  ghmf  18753  ghmlin  18754  conjnsg  18785  gimf1o  18794  gagrpid  18815  gaf  18816  gaass  18818  psgnunilem5  19017  odid  19061  odf1o2  19093  gexid  19101  sylow1lem4  19121  pj1id  19220  efgredeu  19273  ablcmn  19308  cmncom  19318  mulgdi  19343  torsubg  19370  cyggenod2  19400  cygctb  19408  ghmcyg  19412  dprdf1o  19550  ablfacrplem  19583  ablfaclem2  19604  ablfac2  19607  simpg2nsg  19614  fincygsubgodexd  19631  crngmgp  19706  rhmmhm  19881  rhmghm  19884  drngunit  19911  drngmgp  19918  drngid  19920  subrgss  19940  subrg1cl  19947  issubdrg  19964  cntzsdrg  19985  abvge0  20000  srngcnv  20028  lmhmlin  20212  lmimf1o  20240  lvecdrng  20282  lspsolvlem  20319  islbs3  20332  lbsextlem3  20337  2idlcpbl  20418  nzrnz  20444  opprnzr  20449  rrgeq0i  20473  domneq0  20481  domnrrg  20484  drngdomn  20487  fldidomOLD  20490  zringunit  20600  prmirredlem  20606  znidomb  20681  cygzn  20690  psgndiflemB  20717  pjf  20830  frlmsslsp  20913  frlmlbs  20914  f1lindf  20939  assalem  20974  psrbaglefi  21045  mplelsfi  21111  mplsubrglem  21120  mplcoe1  21148  mplbas2  21153  opsrtoslem2  21173  mhpmulcl  21249  coe1mul2  21350  pmatcoe1fsupp  21758  toponuni  21971  tpsuni  21993  mretopd  22151  neips  22172  neiptoptop  22190  neiptopnei  22191  perflp  22213  perfi  22214  cnf  22305  cnpf  22306  cnpimaex  22315  cnima  22324  t0sep  22383  t1ficld  22386  hausnei  22387  pnrmcld  22401  cnrmi  22419  cmpcov  22448  tgcmp  22460  hauscmplem  22465  connclo  22474  1stcclb  22503  2ndcdisj  22515  llyi  22533  nllyi  22534  ptpjpre1  22630  ptpjcn  22670  ptpjopn  22671  ptclsg  22674  dfac14  22677  txdis1cn  22694  pthaus  22697  hauseqlcld  22705  txkgen  22711  xkococn  22719  txconn  22748  hmeocnvcn  22820  fbssfi  22896  filss  22912  uffixfr  22982  flimneiss  23025  flimelbas  23027  flimfnfcls  23087  alexsubb  23105  alexsubALT  23110  ptcmplem2  23112  ptcmplem3  23113  ptcmplem4  23114  tmdgsum2  23155  ghmcnp  23174  tgpt0  23178  qustgplem  23180  istdrg2  23237  vscacn  23245  tvctdrg  23252  uspreg  23334  ucncn  23345  neipcfilu  23356  cuspcvg  23361  psmetxrge0  23374  isxmet2d  23388  prdsxmetlem  23429  imasdsf1olem  23434  xmstopn  23512  mstopn  23513  stdbdxmet  23577  prdsxmslem2  23591  nrgabv  23731  nmvs  23746  nvclvec  23767  nmoge0  23791  nghmcl  23797  nmoi  23798  nghmghm  23804  nmhmlmhm  23819  nmhmnghm  23820  icccmp  23894  xrge0gsumle  23902  metds0  23919  metdstri  23920  metdsre  23922  metdseq0  23923  metdscnlem  23924  metnrmlem1a  23927  icopnfcnv  24011  xrhmeo  24015  pcoval1  24082  cvslvec  24194  cvsunit  24200  cphreccllem  24247  cphsscph  24320  cmetcvg  24354  lmle  24370  cmscmet  24415  cmetcusp1  24422  hlcph  24433  minveclem4  24501  ivthlem3  24522  ovolmge0  24546  ovolicc1  24585  ovolicc2lem3  24588  ovolicc2lem5  24590  dyadmbl  24669  i1ff  24745  i1frn  24746  i1fima2  24748  itg2monolem1  24820  dvnres  25000  c1liplem1  25065  c1lip2  25067  dvge0  25075  lhop1lem  25082  itgsubstlem  25117  fta1glem2  25236  fta1b  25239  plyf  25264  plypf1  25278  plyadd  25283  plymul  25284  coeeu  25291  dgrlem  25295  coeid  25304  elqaalem3  25386  aareccl  25391  eff1olem  25609  relogf1o  25627  logdmn0  25700  logcnlem2  25703  logcnlem3  25704  efopnlem1  25716  efopnlem2  25717  logtayl2  25722  cxpcn3lem  25805  cxpcn3  25806  logbgcd1irr  25849  atandmneg  25961  atandmcj  25964  efiatan2  25972  cosatan  25976  cosatanne0  25977  dvatan  25990  areage0  26018  cxp2lim  26031  jensenlem2  26042  jensen  26043  eldmgm  26076  dmgmaddn0  26077  dmlogdmgm  26078  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgambdd  26091  lgamucov  26092  ftalem3  26129  efnnfsumcl  26157  efchtdvds  26213  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsflf1o  26241  musum  26245  muinv  26247  dvdsmulf1o  26248  lgsfle1  26359  lgsle1  26365  lgsdirprm  26384  lgsne0  26388  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem2  26434  chebbnd1  26525  chtppilim  26528  chpchtlim  26532  chpo1ub  26533  dchrmusumlema  26546  dchrvmasumlem1  26548  dchrisum0lema  26567  dchrisum0lem2a  26570  logsqvma  26595  selberg3lem2  26611  pntrsumo1  26618  pnt2  26666  ostthlem1  26680  ostth3  26691  axtgcgrrflx  26727  axtgcgrid  26728  axtgsegcon  26729  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  tglng  26811  axcontlem7  27241  axcontlem10  27244  upgrle  27363  umgredg2  27373  lfgredgge2  27397  usgredg2ALT  27463  usgr1vr  27525  usgrexmpledg  27532  upgrres1  27583  fusgrvtxfi  27589  vtxnbuvtx  27661  cusgrcplgr  27690  vdumgr0  27750  vtxdgoddnumeven  27823  trlres  27970  usgr2pth  28033  cyclispthon  28070  clwwlknlen  28297  clwwnonrepclwwnon  28610  2clwwlk2  28613  ablocom  28811  phpar2  29086  cbncms  29128  hlph  29152  hcaucvg  29449  hlimconvi  29454  shaddcl  29480  shmulcl  29481  chlimi  29497  chcompl  29505  choc1  29590  nmopre  30133  cnopc  30176  lnopl  30177  unop  30178  hmop  30185  cnfnc  30193  lnfnl  30194  nlelshi  30323  cnlnadjlem5  30334  elpjidm  30447  mdslle1i  30580  mdslle2i  30581  atcv0  30605  chpssati  30626  fovcld  30876  aciunf1lem  30901  padct  30956  ssnnssfz  31010  ccatf1  31125  swrdrndisj  31131  ressprs  31143  oduprs  31144  resspos  31146  resstos  31147  pwrssmgc  31180  ogrpinv0le  31243  ogrpsub  31244  ogrpaddlt  31245  cyc3evpm  31319  cycpmgcl  31322  cycpmconjslem2  31324  cyc3conja  31326  isarchi3  31343  archirng  31344  archirngz  31345  archiabllem1a  31347  archiabllem1b  31348  archiabllem2a  31350  archiabllem2c  31351  archiabllem2b  31352  archiabl  31354  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  ofldtos  31412  ofldlt1  31414  ofldchr  31415  suborng  31416  subofld  31417  isarchiofld  31418  nn0omnd  31447  quslsm  31495  nsgmgclem  31498  nsgmgc  31499  prmidl0  31528  qsidomlem1  31530  krull  31545  sradrng  31575  extdg1id  31640  madjusmdetlem4  31682  qtophaus  31688  crefi  31699  cmpcref  31702  cmppcmp  31710  pcmplfin  31712  zart0  31731  tpr2rico  31764  rge0scvg  31801  zrhunitpreima  31828  qqhrhm  31839  esummono  31922  gsumesum  31927  esumrnmpt2  31936  esumpinfval  31941  esumpcvgval  31946  esumpmono  31947  0elsiga  31982  sigaclcu  31985  issgon  31991  inelpisys  32022  ldsysgenld  32028  ldgenpisyslem1  32031  sxuni  32061  isrnmeas  32068  measvuni  32082  measssd  32083  ddemeas  32104  imambfm  32129  elmbfmvol2  32134  dya2icoseg2  32145  omssubaddlem  32166  omssubadd  32167  carsgsigalem  32182  pmeasmono  32191  sibfinima  32206  oddpwdc  32221  oddpwdcv  32222  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemgvv  32243  eulerpartlemgs2  32247  fiblem  32265  probtot  32279  ballotlem4  32365  ballotlem5  32366  ballotlemfrc  32393  ballotlemirc  32398  ballotth  32404  hgt750lemb  32536  bnj642  32628  bnj643  32629  bnj645  32630  bnj707  32635  bnj1379  32710  bnj1538  32735  bnj110  32738  bnj93  32743  bnj906  32810  bnj1006  32840  bnj1110  32862  bnj1121  32865  bnj1204  32892  bnj1321  32907  bnj1364  32908  bnj1398  32914  bnj1450  32930  bnj1312  32938  bnj1501  32947  bnj1523  32951  0nn0m1nnn0  32971  subfacp1lem3  33044  subfacp1lem5  33046  pconncn  33086  connpconn  33097  cvmcov  33125  cvmliftlem1  33147  cvmliftlem10  33156  cvmlift2lem11  33175  cvmlift2lem12  33176  msubff1  33418  mvhf1  33421  mthmpps  33444  mclspps  33446  fundmpss  33646  tfisg  33692  sltval2  33786  funpartfun  34172  fnetg  34461  neibastop1  34475  filnetlem3  34496  onint1  34565  bj-nnfa  34837  bj-idres  35258  bj-rvecrr  35395  icorempo  35449  pibt2  35515  wl-nfeqfb  35622  phpreu  35688  fin2solem  35690  fin2so  35691  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  matunitlindf  35702  ptrest  35703  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  dvtan  35754  itg2gt0cn  35759  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  cover2  35799  indexa  35818  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  totbndss  35862  equivtotbnd  35863  isbnd3  35869  totbndbnd  35874  equivbnd  35875  prdsbnd  35878  prdstotbnd  35879  heibor  35906  zrdivrng  36038  crngocom  36086  isfld2  36090  dmncrng  36141  eqvrelrel  36637  disjrel  36768  prter2  36822  toycom  36914  lsateln0  36936  lpssat  36954  lssat  36957  oposlem  37123  olop  37155  omllaw  37184  cvlexch1  37269  dihpN  39277  mapdordlem2  39578  mhphflem  40207  prjspertr  40365  nacsfg  40443  nacsfix  40450  mzpindd  40484  diophrw  40497  diophrex  40513  rexzrexnn0  40542  pell1234qrdich  40599  rmspecnonsq  40645  rmspecfund  40647  rmspecpos  40654  monotoddzzfi  40680  ltrmxnn0  40687  rmxnn  40689  jm2.23  40734  jm3.1lem2  40756  dnnumch3  40788  lnmlssfg  40821  lnmlmic  40829  lnrlnm  40854  lnr2i  40857  lpirlnr  40858  hbtlem6  40870  hbt  40871  mnccoe  40879  idomrootle  40936  proot1mul  40940  proot1hash  40941  deg1mhm  40948  ntrneifv2  41579  grucollcld  41767  mnurndlem1  41788  ismnushort  41808  radcnvrat  41821  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  ordelordALT  42046  2uasbanh  42070  ordelordALTVD  42376  elixpconstg  42528  rabidim2  42541  foelrnf  42613  disjinfi  42620  supminfxr2  42899  sumnnodd  43061  stoweidlem7  43438  stoweidlem14  43445  stoweidlem16  43447  stoweidlem24  43455  stoweidlem31  43462  stoweidlem54  43485  wallispilem3  43498  fourierdlem42  43580  fourierdlem48  43585  fourierdlem51  43588  fourierdlem64  43601  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem87  43624  etransclem28  43693  etransclem32  43697  sge0fodjrnlem  43844  hoidmvlelem3  44025  pimrecltpos  44133  pimrecltneg  44147  issmflem  44150  smfaddlem1  44185  smfsuplem1  44231  smfsuplem3  44233  smflimsuplem7  44246  smfliminflem  44250  nfunsnafv  44521  faovcl  44579  tz6.12-2-afv2  44616  tz6.12i-afv2  44622  sprel  44824  evendiv2z  44972  oddp1div2z  44973  2dvdseven  44993  2ndvdsodd  44995  perfectALTVlem1  45061  sbgoldbm  45124  clintopcllaw  45293  0ringbas  45317  rnghmmgmhm  45340  uzlidlring  45375  rnghmsubcsetclem1  45421  rngccatidALTV  45435  zrinitorngc  45446  zrtermorngc  45447  rhmsubcsetclem1  45467  funcringcsetcALTV2lem7  45488  ringccatidALTV  45498  funcringcsetclem7ALTV  45511  irinitoringc  45515  zrtermoringc  45516  fldhmsubc  45530  fldhmsubcALTV  45548  ssnn0ssfz  45573  el0ldepsnzr  45696  regt1loggt0  45770  elbigodm  45789  fllogbd  45794  rrx2xpref1o  45952  unilbss  46051  fdomne0  46065  f002  46069  thincmo2  46197  thincmoALT  46199  fullthinc  46215  elsetrecslem  46290