MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprbi Structured version   Visualization version   Unicode version

Theorem simprbi 471
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
StepHypRef Expression
1 simprbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 199 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 470 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  xornan  1439  sb1  1808  eumo  2348  reurmo  2996  pssne  3515  pssn2lp  3520  ssnpss  3522  eldifn  3545  elinel2  3611  elin2d  3614  rabsnt  4040  eldifsni  4089  unimax  4225  ssintub  4244  moop2  4696  pwssun  4745  weso  4830  opelxp2  4873  eldmeldmressn  5151  wfisg  5422  ordwe  5443  funmo  5605  funopg  5621  funun  5631  fununi  5659  funimaexg  5670  fndm  5685  frn  5747  f1ss  5797  f1ssr  5798  f1ssres  5799  forn  5809  f1f1orn  5839  f1orescnv  5843  f1imacnv  5844  funcocnv2  5852  dffv2  5953  exfo  6055  foelrn  6056  isorel  6235  isoini2  6248  f1ofveu  6303  fovcl  6420  f1opw  6542  onminesb  6644  onminsb  6645  tfis  6700  limomss  6716  nnlim  6724  ssnlim  6729  curry1  6907  curry2  6910  f1o2ndf1  6923  fnwelem  6930  ressuppss  6953  mpt2xopn0yelv  6978  wfrlem5  7058  tz7.48lem  7176  dif20el  7225  oeordi  7306  oeeulem  7320  oeeui  7321  nnawordex  7356  swoer  7409  erdisj  7429  eceqoveq  7486  mapsnconst  7535  ixpn0  7572  resixpfo  7578  boxcutc  7583  sdomnen  7616  en0  7650  en1  7654  domunsncan  7690  fodomr  7741  phplem4  7772  php3  7776  unxpdomlem3  7796  fineqvlem  7804  f1opwfi  7896  fsuppcolem  7932  fsuppco  7933  mapfienlem1  7936  mapfienlem2  7937  supub  7991  suplub  7992  ordtypelem2  8052  ordtypelem3  8053  ordtypelem6  8056  ordtypelem7  8057  wemapso2lem  8085  wdom2d  8113  brwdom3  8115  ixpiunwdom  8124  inf3lem2  8152  inf3lem6  8156  oancom  8174  infdifsn  8180  cantnfp1lem3  8203  cantnflem3  8214  cantnflem4  8215  oef1o  8221  cnfcom3  8227  tctr  8242  tz9.12lem3  8278  scottex  8374  cardid2  8405  infxpenlem  8462  acni3  8496  cardaleph  8538  iscard3  8542  dfac5lem4  8575  dfac5lem5  8576  kmlem1  8598  cofsmo  8717  fin4en1  8757  enfin2i  8769  fin23lem28  8788  fin23lem38  8797  isf32lem6  8806  enfin1ai  8832  isfin1-3  8834  hsmexlem2  8875  hsmexlem4  8877  domtriomlem  8890  axdc2lem  8896  axdc3lem2  8899  ac6num  8927  zorn2lem2  8945  brdom3  8974  alephval2  9015  alephreg  9025  pwcfsdom  9026  smobeth  9029  fpwwe2lem6  9078  fpwwe2lem13  9085  canthp1lem2  9096  pwfseqlem3  9103  hargch  9116  winalim2  9139  gchina  9142  inar1  9218  0npi  9325  mulclpi  9336  mulcanpi  9343  nlt1pi  9349  nqereu  9372  prcdnq  9436  prnmax  9438  ltresr2  9583  axrnegex  9604  axpre-sup  9611  1nuz2  11257  zsupss  11276  rpgt0  11336  ixxss1  11678  ixxss2  11679  ixxss12  11680  lbioo  11692  ubioo  11693  iccss2  11730  iccssico2  11733  elfzuz3  11823  uzdisj  11893  nn0disj  11932  serge0  12305  expge0  12346  expge1  12347  expaddzlem  12353  hashrabsn1  12591  hashfun  12650  cshinj  12967  relexpuzrel  13192  shftfn  13213  sqrlem6  13388  rlimss  13643  lo1dm  13660  o1dm  13671  rlimrege0  13720  fsumf1o  13866  fsumge0  13932  incexc2  13973  supcvg  13991  fprodf1o  14077  divalglem9  14460  divalglem9OLD  14461  bitsfzolem  14486  bitsfzolemOLD  14487  bitsinv2  14496  bitsf1ocnv  14497  bitsf1  14499  gcdcllem1  14552  bezout  14589  prmind2  14714  nprm  14717  sqnprm  14725  dvdsprm  14726  isprm5  14730  coprm  14736  phibndlem  14797  dfphi2  14801  phimullem  14806  pclem  14867  pcpre1  14871  pcidlem  14900  expnprm  14926  prmreclem1  14939  prmreclem2  14940  prmreclem5  14943  1arith  14950  4sqlem18OLD  14985  4sqlem18  14991  vdwnnlem3  15026  ramtlecl  15030  rami  15051  0ram  15057  ramub1lem1  15063  prmgaplem5  15104  firest  15409  acsfiel  15638  isacs1i  15641  catlid  15667  catrid  15668  fullfo  15895  fthf1  15900  fthoppc  15906  invfuc  15957  prslem  16254  posi  16273  dlatmjdi  16518  pslem  16530  tsrlin  16543  cnvtsr  16546  tsrdir  16562  mndid  16627  mhmf  16665  mhmlin  16667  mhm0  16668  mrcmndind  16691  grpinvex  16759  grplinv  16790  mulgz  16857  mulgdirlem  16860  mulgdir  16861  mulgass  16866  nsgbi  16926  nmzbi  16935  ghmf  16965  ghmlin  16966  conjnsg  16996  gimf1o  17005  gagrpid  17026  gaf  17027  gaass  17029  psgnunilem5  17213  odid  17265  odidOLD  17281  odf1o2  17300  gexid  17310  sylow1lem4  17331  odcau  17334  pj1id  17427  efgredeu  17480  ablcmn  17514  cmncom  17524  mulgdi  17545  gexexlem  17568  torsubg  17570  cyggenod2  17598  cygctb  17604  ghmcyg  17608  dprdf1o  17743  dprd2dlem1  17752  dprd2da  17753  ablfacrplem  17776  ablfaclem2  17797  ablfac2  17800  crngmgp  17866  rhmmhm  18028  rhmghm  18031  drngunit  18058  drngmgp  18065  drngid  18067  subrgss  18087  subrg1cl  18094  issubdrg  18111  abvge0  18131  srngcnv  18159  lmhmlin  18336  lmimf1o  18364  lvecdrng  18406  lspsolvlem  18443  islbs3  18456  lbsextlem3  18461  2idlcpbl  18535  nzrnz  18561  opprnzr  18566  rrgeq0i  18590  domneq0  18598  domnrrg  18601  drngdomn  18604  fldidom  18606  assalem  18617  mplsubrglem  18740  mplcoe1  18766  mplbas2  18771  opsrtoslem2  18785  mplelsfi  18791  coe1mul2  18939  zringunit  19139  prmirredlem  19141  znidomb  19209  cygzn  19218  psgndiflemB  19245  pjf  19353  frlmsslsp  19431  frlmlbs  19432  f1lindf  19457  pmatcoe1fsupp  19802  toponuni  20019  tpsuni  20030  clsval2  20142  mretopd  20185  neips  20206  neiptoptop  20224  neiptopnei  20225  perflp  20247  perfi  20248  restfpw  20272  cnf  20339  cnpf  20340  cnpimaex  20349  cnima  20358  t0sep  20417  t1sncld  20419  t1ficld  20420  hausnei  20421  regsep  20427  pnrmcld  20435  nrmsep3  20448  cnrmi  20453  cmpcov  20481  discmp  20490  tgcmp  20493  uncmp  20495  hauscmplem  20498  cmpfi  20500  conclo  20507  1stcclb  20536  2ndcdisj  20548  llyi  20566  nllyi  20567  ptpjpre1  20663  ptpjcn  20703  ptpjopn  20704  ptclsg  20707  dfac14  20710  txdis1cn  20727  pthaus  20730  hauseqlcld  20738  txkgen  20744  xkococn  20752  txcon  20781  hmeocnvcn  20853  fbssfi  20930  filss  20946  ufilss  20998  uffixfr  21016  flimneiss  21059  flimelbas  21061  fclscf  21118  flimfnfcls  21121  alexsublem  21137  alexsubb  21139  alexsubALT  21144  ptcmplem2  21146  ptcmplem3  21147  ptcmplem4  21148  tmdgsum2  21189  ghmcnp  21207  tgpt0  21211  qustgplem  21213  tsmsfbas  21220  tsmslem1  21221  tsmsgsum  21231  tsmssubm  21235  tsmsres  21236  tsmsf1o  21237  tsmsmhm  21238  tsmsadd  21239  tsmsxplem1  21245  tsmsxplem2  21246  tsmsxp  21247  istdrg2  21270  vscacn  21278  tvctdrg  21285  uspreg  21367  ucncn  21378  neipcfilu  21389  cuspcvg  21394  psmetxrge0  21407  isxmet2d  21420  prdsxmetlem  21461  imasdsf1olem  21466  xmstopn  21544  mstopn  21545  stdbdxmet  21608  prdsxmslem2  21622  nrgabv  21742  nmvs  21757  nvclvec  21777  nmoge0  21804  nghmcl  21810  nmoi  21811  nmoge0OLD  21822  nmoiOLD  21827  nghmghm  21833  nmhmlmhm  21848  nmhmnghm  21849  icccmp  21921  xrge0gsumle  21929  xrge0tsms  21930  metds0  21945  metdstri  21946  metdsre  21948  metdseq0  21949  metdscnlem  21950  metnrmlem1a  21953  metds0OLD  21960  metdstriOLD  21961  metdsreOLD  21963  metdseq0OLD  21964  metdscnlemOLD  21965  metnrmlem1aOLD  21968  icopnfcnv  22048  xrhmeo  22052  pcoval1  22122  cvslvec  22215  cvsunit  22217  cphreccllem  22234  cmetcvg  22333  lmle  22349  cmscmet  22392  cmetcusp1  22398  hlcph  22409  minveclem4  22452  minveclem4OLD  22464  ivthlem3  22482  ovolmge0  22508  ovolicc1  22547  ovolicc2lem3  22550  ovolicc2lem5  22553  mblsplit  22564  dyadmbl  22637  mbfdm  22663  mbfadd  22696  mbfsub  22697  i1ff  22713  i1frn  22714  i1fima2  22716  mbfmul  22763  itg2monolem1  22787  bddmulibl  22875  dvnres  22964  c1liplem1  23027  c1lip2  23029  dvge0  23037  lhop1lem  23044  itgsubstlem  23079  fta1glem1  23195  fta1glem2  23196  fta1b  23199  plyf  23231  plypf1  23245  plyadd  23250  plymul  23251  coeeu  23258  dgrlem  23262  coeid  23271  elqaalem3  23353  elqaalem3OLD  23356  aareccl  23361  eff1olem  23576  relogf1o  23595  logdmn0  23664  logcnlem2  23667  logcnlem3  23668  dvloglem  23672  efopnlem1  23680  efopnlem2  23681  logtayl2  23686  cxpcn3lem  23766  cxpcn3  23767  atandmneg  23911  atandmcj  23914  efiatan2  23922  cosatan  23926  cosatanne0  23927  dvatan  23940  areage0  23968  cxp2lim  23981  jensenlem2  23992  jensen  23993  eldmgm  24026  dmgmaddn0  24027  dmlogdmgm  24028  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem5  24037  lgambdd  24041  lgamucov  24042  wilthlem1  24072  wilth  24075  ftalem3  24078  efnnfsumcl  24108  isppw  24120  efchtdvds  24165  sqff1o  24188  dvdsdivcl  24189  fsumdvdsdiaglem  24191  dvdsppwf1o  24194  dvdsflf1o  24195  musum  24199  muinv  24201  dvdsmulf1o  24202  fsumvma2  24221  vmasum  24223  chpval2  24225  chpchtsum  24226  chpub  24227  mersenne  24234  perfect1  24235  bposlem1  24291  bposlem5  24295  lgsfle1  24312  lgsle1  24318  lgsdirprm  24336  lgsne0  24340  lgsqrlem4  24351  lgseisenlem3  24358  lgseisenlem4  24359  lgsquadlem1  24361  lgsquadlem2  24362  2sqblem  24384  chebbnd1lem1  24386  chebbnd1  24389  chtppilim  24392  chpchtlim  24396  chpo1ub  24397  rplogsumlem2  24402  rpvmasumlem  24404  dchrmusumlema  24410  dchrvmasumlem1  24412  dchrisum0flblem2  24426  dchrisum0lema  24431  dchrisum0lem2a  24434  logsqvma  24459  selberg3lem2  24475  pntrsumo1  24482  pnt2  24530  ostthlem1  24544  ostth3  24555  axtgcgrrflx  24589  axtgcgrid  24590  axtgsegcon  24591  axtg5seg  24592  axtgbtwnid  24593  axtgpasch  24594  axtgcont1  24595  tglng  24670  axcontlem7  25079  axcontlem10  25082  umgrale  25127  usgraedg2  25181  usgraexmpledg  25210  clwlkfclwwlk1hashn  25648  eupatrl  25775  gxneg  26075  gxadd  26084  gxmul  26087  ablocom  26094  subgoablo  26120  smgrpisass  26142  mndoisexid  26149  zrdivrng  26241  phpar2  26545  cbncms  26588  hlph  26622  hcaucvg  26920  hlimconvi  26925  shaddcl  26951  shmulcl  26952  chlimi  26968  chcompl  26976  choc1  27061  nmopre  27604  cnopc  27647  lnopl  27648  unop  27649  hmop  27656  cnfnc  27664  lnfnl  27665  nlelshi  27794  cnlnadjlem5  27805  elpjidm  27918  mdslle1i  28051  mdslle2i  28052  atcv0  28076  chpssati  28097  fovcld  28315  aciunf1lem  28339  padct  28382  ssnnssfz  28442  ressprs  28491  oduprs  28492  resspos  28495  resstos  28496  tleile  28497  ogrpinvOLD  28552  ogrpinv0le  28553  ogrpsub  28554  ogrpaddlt  28555  isarchi3  28578  archirng  28579  archirngz  28580  archiabllem1a  28582  archiabllem1b  28583  archiabllem2a  28585  archiabllem2c  28586  archiabllem2b  28587  archiabl  28589  orngsqr  28641  ornglmulle  28642  orngrmulle  28643  ofldtos  28648  ofldlt1  28650  ofldchr  28651  suborng  28652  subofld  28653  isarchiofld  28654  nn0omnd  28678  madjusmdetlem4  28730  qtophaus  28737  crefi  28748  cmpcref  28751  cmppcmp  28759  pcmplfin  28761  tpr2rico  28792  rge0scvg  28829  zrhunitpreima  28856  qqhrhm  28867  esummono  28949  gsumesum  28954  esumrnmpt2  28963  esumpinfval  28968  esumpcvgval  28973  esumpmono  28974  0elsiga  29010  sigaclcu  29013  issgon  29019  inelpisys  29050  ldsysgenld  29056  ldgenpisyslem1  29059  sxuni  29089  isrnmeas  29096  measvuni  29110  measssd  29111  ddemeas  29132  imambfm  29157  elmbfmvol2  29162  dya2icoseg2  29173  omssubaddlem  29200  omssubadd  29201  omssubaddlemOLD  29204  omssubaddOLD  29205  carsgsigalem  29220  pmeasmono  29230  sibfinima  29245  oddpwdc  29260  oddpwdcv  29261  eulerpartlemf  29276  eulerpartlemt  29277  eulerpartlemr  29280  eulerpartlemgvv  29282  eulerpartlemgs2  29286  sseqf  29298  fiblem  29304  probtot  29318  ballotlem4  29404  ballotlem5  29405  ballotlemfrc  29432  ballotlemirc  29437  ballotth  29443  ballotlemfrcOLD  29470  ballotlemircOLD  29475  ballotthOLD  29481  bnj642  29630  bnj643  29631  bnj645  29632  bnj707  29637  bnj1379  29714  bnj1538  29738  bnj110  29741  bnj93  29746  bnj906  29813  bnj1006  29842  bnj1110  29863  bnj1121  29866  bnj1172  29882  bnj1204  29893  bnj1321  29908  bnj1364  29909  bnj1398  29915  bnj1450  29931  bnj1312  29939  bnj1501  29948  bnj1523  29952  subfacp1lem3  29977  subfacp1lem5  29979  pconcn  30019  sconpht  30024  conpcon  30030  cvmcov  30058  cvmliftlem1  30080  cvmliftlem10  30089  cvmlift2lem11  30108  cvmlift2lem12  30109  msubff1  30266  mvhf1  30269  mthmpps  30292  mclspps  30294  fundmpss  30478  tfisg  30528  frinsg  30554  frrlem5  30589  sltval2  30614  txpss3v  30716  pprodss4v  30722  fnetg  31072  neibastop1  31086  filnetlem3  31107  onint1  31180  bj-elid2  31711  icorempt2  31824  wl-nfeqfb  31940  phpreu  31993  fin2solem  31995  fin2so  31996  ptrest  32003  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem5  32009  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem9  32013  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem13  32017  poimirlem14  32018  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem29  32033  poimirlem31  32035  mblfinlem2  32042  dvtan  32056  itg2gt0cn  32061  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  cover2  32104  indexa  32124  istotbnd3  32167  sstotbnd2  32170  sstotbnd  32171  totbndss  32173  equivtotbnd  32174  isbnd3  32180  totbndbnd  32185  equivbnd  32186  prdsbnd  32189  prdstotbnd  32190  heibor  32217  crngocom  32298  isfld2  32302  dmncrng  32353  prter2  32517  toycom  32610  lsateln0  32632  lpssat  32650  lssat  32653  oposlem  32819  olop  32851  omllaw  32880  cvlexch1  32965  dihpN  34975  mapdordlem2  35276  nacsfg  35618  nacsfix  35625  mzpindd  35659  diophrw  35672  diophrex  35689  rexzrexnn0  35718  pell1234qrdich  35778  rmspecsqrtnq  35825  rmspecnonsq  35826  rmspecfund  35828  rmspecpos  35835  monotoddzzfi  35861  ltrmxnn0  35870  rmxnn  35872  jm2.23  35922  jm3.1lem2  35944  dnnumch3  35976  lnmlssfg  36009  lnmlmic  36017  lnrlnm  36043  lnr2i  36046  lpirlnr  36047  hbtlem6  36059  hbt  36060  mnccoe  36068  cntzsdrg  36139  idomrootle  36140  proot1mul  36144  phisum  36147  proot1hash  36148  deg1mhm  36155  radcnvrat  36733  binomcxplemdvbinom  36772  binomcxplemcvg  36773  binomcxplemnotnn0  36775  ordelordALT  36968  2uasbanh  36998  ordelordALTVD  37327  foelrnf  37532  disjinfi  37539  sumnnodd  37807  stoweidlem7  37979  stoweidlem14  37986  stoweidlem16  37988  stoweidlem24  37996  stoweidlem31  38004  stoweidlem54  38027  wallispilem3  38041  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem48  38130  fourierdlem51  38133  fourierdlem64  38146  fourierdlem76  38158  fourierdlem79  38161  fourierdlem81  38163  fourierdlem87  38169  etransclem28  38239  etransclem32  38243  sge0fodjrnlem  38372  hoidmvlelem3  38537  2reu1  38752  nfunsnafv  38789  faovcl  38847  evendiv2z  38906  oddp1div2z  38907  2dvdseven  38928  2ndvdsodd  38929  perfectALTVlem1  38988  upgrle  39336  umgredg2  39345  lfgredgge2  39369  usgredg2ALT  39438  usgrexmpledg  39498  upgrres1  39544  fusgrvtxfi  39550  nbfusgrlevtxm1  39615  nbfusgrlevtxm2  39616  cusgrcplgr  39652  trlres  39896  umgrn1cycl  39985  usgra2pth  40176  clintopcllaw  40355  0ringbas  40379  rnghmmgmhm  40402  uzlidlring  40437  rnghmsubcsetclem1  40485  rngccatidALTV  40499  zrinitorngc  40510  zrtermorngc  40511  rhmsubcsetclem1  40531  funcringcsetcALTV2lem7  40552  ringccatidALTV  40562  funcringcsetclem7ALTV  40575  irinitoringc  40579  zrtermoringc  40580  fldhmsubc  40594  fldhmsubcALTV  40613  ssnn0ssfz  40638  el0ldepsnzr  40768  eluz2gt1  40813  regt1loggt0  40855  elbigodm  40874  fllogbd  40879
  Copyright terms: Public domain W3C validator