Theorem simprbi 480

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simprbi	|- ( ph -> ch )

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 206	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 479	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  xornan  1472  sb1  1883  eumo  2499  reurmo  3161  pssne  3703  pssn2lp  3708  ssnpss  3710  eldifn  3733  elinel2  3800  rabsnt  4266  eldifsni  4320  unimax  4473  ssintub  4495  moop2  4966  pwssun  5020  weso  5105  opelxp2  5151  wfisg  5715  ordwe  5736  funmo  5904  funopg  5922  funun  5932  fununi  5964  funimaexg  5975  fndm  5990  frn  6053  f1ss  6106  f1ssr  6107  f1ssres  6108  forn  6118  f1f1orn  6148  f1orescnv  6152  f1imacnv  6153  funcocnv2  6161  dffv2  6271  exfo  6377  foelrn  6378  isorel  6576  isoini2  6589  f1ofveu  6645  fovcl  6765  f1opw  6889  onminesb  6998  onminsb  6999  tfis  7054  limomss  7070  nnlim  7078  ssnlim  7083  curry1  7269  curry2  7272  f1o2ndf1  7285  fnwelem  7292  ressuppss  7314  mpt2xopn0yelv  7339  wfrlem5  7419  tz7.48lem  7536  dif20el  7585  oeordi  7667  oeeulem  7681  oeeui  7682  nnawordex  7717  swoer  7772  erdisj  7794  eceqoveq  7853  mapsnconst  7903  resixpfo  7946  boxcutc  7951  sdomnen  7984  en0  8019  en1  8023  domunsncan  8060  fodomr  8111  phplem4  8142  php3  8146  unxpdomlem3  8166  fineqvlem  8174  f1opwfi  8270  fsuppcolem  8306  fsuppco  8307  mapfienlem1  8310  mapfienlem2  8311  supub  8365  suplub  8366  ordtypelem2  8424  ordtypelem3  8425  ordtypelem6  8428  ordtypelem7  8429  wemapso2lem  8457  wdom2d  8485  brwdom3  8487  ixpiunwdom  8496  inf3lem2  8526  inf3lem6  8530  oancom  8548  infdifsn  8554  cantnfp1lem3  8577  cantnflem3  8588  cantnflem4  8589  oef1o  8595  cnfcom3  8601  tctr  8616  tz9.12lem3  8652  scottex  8748  cardid2  8779  infxpenlem  8836  acni3  8870  cardaleph  8912  iscard3  8916  dfac5lem4  8949  dfac5lem5  8950  kmlem1  8972  cofsmo  9091  fin4en1  9131  enfin2i  9143  fin23lem28  9162  fin23lem38  9171  isf32lem6  9180  enfin1ai  9206  isfin1-3  9208  hsmexlem2  9249  hsmexlem4  9251  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  ac6num  9301  zorn2lem2  9319  brdom3  9350  alephval2  9394  alephreg  9404  pwcfsdom  9405  smobeth  9408  fpwwe2lem6  9457  fpwwe2lem13  9464  canthp1lem2  9475  pwfseqlem3  9482  hargch  9495  winalim2  9518  gchina  9521  inar1  9597  0npi  9704  mulclpi  9715  mulcanpi  9722  nlt1pi  9728  nqereu  9751  prcdnq  9815  prnmax  9817  ltresr2  9962  axrnegex  9983  axpre-sup  9990  eluz2gt1  11760  1nuz2  11764  zsupss  11777  rpgt0  11844  ixxss1  12193  ixxss2  12194  ixxss12  12195  lbioo  12206  ubioo  12207  iccss2  12244  iccssico2  12247  elfzuz3  12339  uzdisj  12413  nn0disj  12455  serge0  12855  expge0  12896  expge1  12897  expaddzlem  12903  hashrabsn1  13163  hashfun  13224  cshinj  13557  relexpuzrel  13792  shftfn  13813  sqrlem6  13988  rlimss  14233  lo1dm  14250  o1dm  14261  rlimrege0  14310  fsumf1o  14454  fsumge0  14527  incexc2  14570  supcvg  14588  fprodf1o  14676  divalglem9  15124  bitsfzolem  15156  bitsinv2  15165  bitsf1ocnv  15166  bitsf1  15168  gcdcllem1  15221  bezout  15260  prmind2  15398  nprm  15401  sqnprm  15414  dvdsprm  15415  isprm5  15419  coprm  15423  phibndlem  15475  dfphi2  15479  phimullem  15484  phisum  15495  pclem  15543  pcpre1  15547  pcidlem  15576  expnprm  15606  prmreclem1  15620  prmreclem2  15621  prmreclem5  15624  1arith  15631  4sqlem18  15666  vdwnnlem3  15701  ramtlecl  15704  rami  15719  0ram  15724  ramub1lem1  15730  prmgaplem5  15759  firest  16093  acsfiel  16315  isacs1i  16318  catlid  16344  catrid  16345  fullfo  16572  fthf1  16577  fthoppc  16583  invfuc  16634  prslem  16931  posi  16950  dlatmjdi  17194  pslem  17206  tsrlin  17219  cnvtsr  17222  tsrdir  17238  mndid  17303  mhmf  17340  mhmlin  17342  mhm0  17343  mrcmndind  17366  grpinvex  17432  grplinv  17468  mulgz  17568  mulgdirlem  17572  mulgdir  17573  mulgass  17579  nsgbi  17625  nmzbi  17634  ghmf  17664  ghmlin  17665  conjnsg  17696  gimf1o  17705  gagrpid  17727  gaf  17728  gaass  17730  psgnunilem5  17914  odid  17957  odf1o2  17988  gexid  17996  sylow1lem4  18016  odcau  18019  pj1id  18112  efgredeu  18165  ablcmn  18199  cmncom  18209  mulgdi  18232  gexexlem  18255  torsubg  18257  cyggenod2  18287  cygctb  18293  ghmcyg  18297  dprdf1o  18431  dprd2dlem1  18440  dprd2da  18441  ablfacrplem  18464  ablfaclem2  18485  ablfac2  18488  crngmgp  18555  rhmmhm  18722  rhmghm  18725  drngunit  18752  drngmgp  18759  drngid  18761  subrgss  18781  subrg1cl  18788  issubdrg  18805  abvge0  18825  srngcnv  18853  lmhmlin  19035  lmimf1o  19063  lvecdrng  19105  lspsolvlem  19142  islbs3  19155  lbsextlem3  19160  2idlcpbl  19234  nzrnz  19260  opprnzr  19265  rrgeq0i  19289  domneq0  19297  domnrrg  19300  drngdomn  19303  fldidom  19305  assalem  19316  mplsubrglem  19439  mplcoe1  19465  mplbas2  19470  opsrtoslem2  19485  mplelsfi  19491  coe1mul2  19639  zringunit  19836  prmirredlem  19841  znidomb  19910  cygzn  19919  psgndiflemB  19946  pjf  20057  frlmsslsp  20135  frlmlbs  20136  f1lindf  20161  pmatcoe1fsupp  20506  toponuni  20719  tpsuni  20740  clsval2  20854  mretopd  20896  neips  20917  neiptoptop  20935  neiptopnei  20936  perflp  20958  perfi  20959  restfpw  20983  cnf  21050  cnpf  21051  cnpimaex  21060  cnima  21069  t0sep  21128  t1ficld  21131  hausnei  21132  pnrmcld  21146  cnrmi  21164  cmpcov  21192  discmp  21201  tgcmp  21204  uncmp  21206  hauscmplem  21209  cmpfi  21211  connclo  21218  1stcclb  21247  2ndcdisj  21259  llyi  21277  nllyi  21278  ptpjpre1  21374  ptpjcn  21414  ptpjopn  21415  ptclsg  21418  dfac14  21421  txdis1cn  21438  pthaus  21441  hauseqlcld  21449  txkgen  21455  xkococn  21463  txconn  21492  hmeocnvcn  21564  fbssfi  21641  filss  21657  ufilss  21709  uffixfr  21727  flimneiss  21770  flimelbas  21772  fclscf  21829  flimfnfcls  21832  alexsublem  21848  alexsubb  21850  alexsubALT  21855  ptcmplem2  21857  ptcmplem3  21858  ptcmplem4  21859  tmdgsum2  21900  ghmcnp  21918  tgpt0  21922  qustgplem  21924  tsmsfbas  21931  tsmslem1  21932  tsmsgsum  21942  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  tsmsmhm  21949  tsmsadd  21950  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  istdrg2  21981  vscacn  21989  tvctdrg  21996  uspreg  22078  ucncn  22089  neipcfilu  22100  cuspcvg  22105  psmetxrge0  22118  isxmet2d  22132  prdsxmetlem  22173  imasdsf1olem  22178  xmstopn  22256  mstopn  22257  stdbdxmet  22320  prdsxmslem2  22334  nrgabv  22465  nmvs  22480  nvclvec  22501  nmoge0  22525  nghmcl  22531  nmoi  22532  nghmghm  22538  nmhmlmhm  22553  nmhmnghm  22554  icccmp  22628  xrge0gsumle  22636  xrge0tsms  22637  metds0  22653  metdstri  22654  metdsre  22656  metdseq0  22657  metdscnlem  22658  metnrmlem1a  22661  icopnfcnv  22741  xrhmeo  22745  pcoval1  22813  cvslvec  22925  cvsunit  22931  cphreccllem  22978  cmetcvg  23083  lmle  23099  cmscmet  23143  cmetcusp1  23149  hlcph  23160  minveclem4  23203  ivthlem3  23222  ovolmge0  23245  ovolicc1  23284  ovolicc2lem3  23287  ovolicc2lem5  23289  mblsplit  23300  dyadmbl  23368  mbfdm  23395  mbfadd  23428  mbfsub  23429  i1ff  23443  i1frn  23444  i1fima2  23446  mbfmul  23493  itg2monolem1  23517  bddmulibl  23605  dvnres  23694  c1liplem1  23759  c1lip2  23761  dvge0  23769  lhop1lem  23776  itgsubstlem  23811  fta1glem1  23925  fta1glem2  23926  fta1b  23929  plyf  23954  plypf1  23968  plyadd  23973  plymul  23974  coeeu  23981  dgrlem  23985  coeid  23994  elqaalem3  24076  aareccl  24081  eff1olem  24294  relogf1o  24313  logdmn0  24386  logcnlem2  24389  logcnlem3  24390  dvloglem  24394  efopnlem1  24402  efopnlem2  24403  logtayl2  24408  cxpcn3lem  24488  cxpcn3  24489  atandmneg  24633  atandmcj  24636  efiatan2  24644  cosatan  24648  cosatanne0  24649  dvatan  24662  areage0  24690  cxp2lim  24703  jensenlem2  24714  jensen  24715  eldmgm  24748  dmgmaddn0  24749  dmlogdmgm  24750  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  lgamucov  24764  wilthlem1  24794  wilth  24797  ftalem3  24801  efnnfsumcl  24829  isppw  24840  efchtdvds  24885  sqff1o  24908  fsumdvdsdiaglem  24909  dvdsppwf1o  24912  dvdsflf1o  24913  musum  24917  muinv  24919  dvdsmulf1o  24920  fsumvma2  24939  vmasum  24941  chpval2  24943  chpchtsum  24944  chpub  24945  mersenne  24952  perfect1  24953  bposlem1  25009  lgsfle1  25031  lgsle1  25037  lgsdirprm  25056  lgsne0  25060  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  2sqblem  25156  chebbnd1lem1  25158  chebbnd1  25161  chtppilim  25164  chpchtlim  25168  chpo1ub  25169  rplogsumlem2  25174  rpvmasumlem  25176  dchrmusumlema  25182  dchrvmasumlem1  25184  dchrisum0flblem2  25198  dchrisum0lema  25203  dchrisum0lem2a  25206  logsqvma  25231  selberg3lem2  25247  pntrsumo1  25254  pnt2  25302  ostthlem1  25316  ostth3  25327  axtgcgrrflx  25361  axtgcgrid  25362  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  tglng  25441  axcontlem7  25850  axcontlem10  25853  upgrle  25985  umgredg2  25995  lfgredgge2  26019  usgredg2ALT  26085  usgr1vr  26147  usgrexmpledg  26154  upgrres1  26205  fusgrvtxfi  26211  nbfusgrlevtxm1  26279  nbfusgrlevtxm2  26280  cusgrcplgr  26316  vdumgr0  26376  vtxdgoddnumeven  26449  trlres  26597  usgr2pth  26660  umgrn1cycl  26699  clwlksfclwwlk1hashn  26959  ablocom  27402  phpar2  27678  cbncms  27721  hlph  27745  hcaucvg  28043  hlimconvi  28048  shaddcl  28074  shmulcl  28075  chlimi  28091  chcompl  28099  choc1  28186  nmopre  28729  cnopc  28772  lnopl  28773  unop  28774  hmop  28781  cnfnc  28789  lnfnl  28790  nlelshi  28919  cnlnadjlem5  28930  elpjidm  29043  mdslle1i  29176  mdslle2i  29177  atcv0  29201  chpssati  29222  fovcld  29440  aciunf1lem  29462  padct  29497  ssnnssfz  29549  ressprs  29655  oduprs  29656  resspos  29659  resstos  29660  tleile  29661  ogrpinvOLD  29715  ogrpinv0le  29716  ogrpsub  29717  ogrpaddlt  29718  isarchi3  29741  archirng  29742  archirngz  29743  archiabllem1a  29745  archiabllem1b  29746  archiabllem2a  29748  archiabllem2c  29749  archiabllem2b  29750  archiabl  29752  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  ofldtos  29811  ofldlt1  29813  ofldchr  29814  suborng  29815  subofld  29816  isarchiofld  29817  nn0omnd  29841  madjusmdetlem4  29896  qtophaus  29903  crefi  29914  cmpcref  29917  cmppcmp  29925  pcmplfin  29927  tpr2rico  29958  rge0scvg  29995  zrhunitpreima  30022  qqhrhm  30033  esummono  30116  gsumesum  30121  esumrnmpt2  30130  esumpinfval  30135  esumpcvgval  30140  esumpmono  30141  0elsiga  30177  sigaclcu  30180  issgon  30186  inelpisys  30217  ldsysgenld  30223  ldgenpisyslem1  30226  sxuni  30256  isrnmeas  30263  measvuni  30277  measssd  30278  ddemeas  30299  imambfm  30324  elmbfmvol2  30329  dya2icoseg2  30340  omssubaddlem  30361  omssubadd  30362  carsgsigalem  30377  pmeasmono  30386  sibfinima  30401  oddpwdc  30416  oddpwdcv  30417  eulerpartlemf  30432  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgvv  30438  eulerpartlemgs2  30442  sseqf  30454  fiblem  30460  probtot  30474  ballotlem4  30560  ballotlem5  30561  ballotlemfrc  30588  ballotlemirc  30593  ballotth  30599  hgt750lemb  30734  bnj642  30818  bnj643  30819  bnj645  30820  bnj707  30825  bnj1379  30901  bnj1538  30925  bnj110  30928  bnj93  30933  bnj906  31000  bnj1006  31029  bnj1110  31050  bnj1121  31053  bnj1204  31080  bnj1321  31095  bnj1364  31096  bnj1398  31102  bnj1450  31118  bnj1312  31126  bnj1501  31135  bnj1523  31139  subfacp1lem3  31164  subfacp1lem5  31166  pconncn  31206  connpconn  31217  cvmcov  31245  cvmliftlem1  31267  cvmliftlem10  31276  cvmlift2lem11  31295  cvmlift2lem12  31296  msubff1  31453  mvhf1  31456  mthmpps  31479  mclspps  31481  fundmpss  31664  tfisg  31716  frinsg  31742  frrlem5  31784  sltval2  31809  txpss3v  31985  pprodss4v  31991  fnetg  32340  neibastop1  32354  filnetlem3  32375  onint1  32448  bj-elid2  33086  icorempt2  33199  wl-nfeqfb  33323  phpreu  33393  fin2solem  33395  fin2so  33396  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  ptrest  33408  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  mblfinlem2  33447  dvtan  33460  itg2gt0cn  33465  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  cover2  33508  indexa  33528  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  totbndss  33576  equivtotbnd  33577  isbnd3  33583  totbndbnd  33588  equivbnd  33589  prdsbnd  33592  prdstotbnd  33593  heibor  33620  zrdivrng  33752  crngocom  33800  isfld2  33804  dmncrng  33855  xrnss3v  34135  prter2  34166  toycom  34260  lsateln0  34282  lpssat  34300  lssat  34303  oposlem  34469  olop  34501  omllaw  34530  cvlexch1  34615  dihpN  36625  mapdordlem2  36926  nacsfg  37268  nacsfix  37275  mzpindd  37309  diophrw  37322  diophrex  37339  rexzrexnn0  37368  pell1234qrdich  37425  rmspecsqrtnqOLD  37471  rmspecnonsq  37472  rmspecfund  37474  rmspecpos  37481  monotoddzzfi  37507  ltrmxnn0  37516  rmxnn  37518  jm2.23  37563  jm3.1lem2  37585  dnnumch3  37617  lnmlssfg  37650  lnmlmic  37658  lnrlnm  37683  lnr2i  37686  lpirlnr  37687  hbtlem6  37699  hbt  37700  mnccoe  37708  cntzsdrg  37772  idomrootle  37773  proot1mul  37777  proot1hash  37778  deg1mhm  37785  ntrneifv2  38378  radcnvrat  38513  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  ordelordALT  38747  2uasbanh  38777  ordelordALTVD  39103  elixpconstg  39266  rabidim2  39284  foelrnf  39373  disjinfi  39380  supminfxr2  39699  sumnnodd  39862  stoweidlem7  40224  stoweidlem14  40231  stoweidlem16  40233  stoweidlem24  40241  stoweidlem31  40248  stoweidlem54  40271  wallispilem3  40284  fourierdlem42  40366  fourierdlem48  40371  fourierdlem51  40374  fourierdlem64  40387  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem87  40410  etransclem28  40479  etransclem32  40483  sge0fodjrnlem  40633  hoidmvlelem3  40811  preimagelt  40912  preimalegt  40913  pimrecltpos  40919  pimrecltneg  40933  issmflem  40936  smfaddlem1  40971  smfsuplem1  41017  smfsuplem3  41019  smflimsuplem7  41032  smfliminflem  41036  nfunsnafv  41222  faovcl  41280  evendiv2z  41545  oddp1div2z  41546  2dvdseven  41566  2ndvdsodd  41567  perfectALTVlem1  41630  sbgoldbm  41672  sprel  41734  clintopcllaw  41847  0ringbas  41871  rnghmmgmhm  41894  uzlidlring  41929  rnghmsubcsetclem1  41975  rngccatidALTV  41989  zrinitorngc  42000  zrtermorngc  42001  rhmsubcsetclem1  42021  funcringcsetcALTV2lem7  42042  ringccatidALTV  42052  funcringcsetclem7ALTV  42065  irinitoringc  42069  zrtermoringc  42070  fldhmsubc  42084  fldhmsubcALTV  42102  ssnn0ssfz  42127  el0ldepsnzr  42256  regt1loggt0  42330  elbigodm  42349  fllogbd  42354  elsetrecslem  42444