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

Theorem simprbi 465
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 197 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 464 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  xornan  1409  sb1  1789  eumo  2295  2eu1OLD  2351  reurmo  3046  pssne  3561  pssn2lp  3566  ssnpss  3568  eldifn  3588  elinel2  3652  rabsnt  4074  eldifsni  4123  unimax  4251  ssintub  4270  moop2  4712  pwssun  4756  weso  4841  opelxp2  4884  eldmeldmressn  5161  wfisg  5431  ordwe  5452  funmo  5614  funopg  5630  funun  5640  fununi  5664  funimaexg  5675  fndm  5690  frn  5749  f1ss  5798  f1ssr  5799  f1ssres  5800  forn  5810  f1f1orn  5839  f1orescnv  5843  f1imacnv  5844  funcocnv2  5852  dffv2  5951  exfo  6052  foelrn  6053  isorel  6229  isoini2  6242  f1ofveu  6297  fovcl  6412  f1opw  6534  onminesb  6636  onminsb  6637  tfis  6692  limomss  6708  nnlim  6716  ssnlim  6721  curry1  6896  curry2  6899  f1o2ndf1  6912  fnwelem  6919  ressuppss  6942  mpt2xopn0yelv  6964  wfrlem5  7045  tz7.48lem  7163  dif20el  7212  oeordi  7293  oeeulem  7307  oeeui  7308  nnawordex  7343  swoer  7396  erdisj  7416  eceqoveq  7473  mapsnconst  7522  ixpn0  7559  resixpfo  7565  boxcutc  7570  sdomnen  7602  en0  7636  en1  7640  domunsncan  7675  fodomr  7726  phplem4  7757  php3  7761  unxpdomlem3  7781  fineqvlem  7789  f1opwfi  7881  fsuppcolem  7917  fsuppco  7918  mapfienlem1  7921  mapfienlem2  7922  supub  7976  suplub  7977  ordtypelem2  8037  ordtypelem3  8038  ordtypelem6  8041  ordtypelem7  8042  wemapso2lem  8070  wdom2d  8098  brwdom3  8100  ixpiunwdom  8109  inf3lem2  8137  inf3lem6  8141  oancom  8159  infdifsn  8164  cantnfp1lem3  8187  cantnflem3  8198  cantnflem4  8199  oef1o  8205  cnfcom3  8211  tctr  8226  tz9.12lem3  8262  scottex  8358  cardid2  8389  infxpenlem  8446  acni3  8479  cardaleph  8521  iscard3  8525  dfac5lem4  8558  dfac5lem5  8559  kmlem1  8581  cofsmo  8700  fin4en1  8740  enfin2i  8752  fin23lem28  8771  fin23lem38  8780  isf32lem6  8789  enfin1ai  8815  isfin1-3  8817  hsmexlem2  8858  hsmexlem4  8860  domtriomlem  8873  axdc2lem  8879  axdc3lem2  8882  ac6num  8910  zorn2lem2  8928  brdom3  8957  alephval2  8998  alephreg  9008  pwcfsdom  9009  smobeth  9012  fpwwe2lem6  9061  fpwwe2lem13  9068  canthp1lem2  9079  pwfseqlem3  9086  hargch  9099  winalim2  9122  gchina  9125  inar1  9201  0npi  9308  mulclpi  9319  mulcanpi  9326  nlt1pi  9332  nqereu  9355  prcdnq  9419  prnmax  9421  ltresr2  9566  axrnegex  9587  axpre-sup  9594  1nuz2  11235  zsupss  11254  rpgt0  11314  ixxss1  11654  ixxss2  11655  ixxss12  11656  lbioo  11668  ubioo  11669  iccss2  11706  iccssico2  11709  elfzuz3  11798  uzdisj  11868  nn0disj  11908  serge0  12267  expge0  12308  expge1  12309  expaddzlem  12315  hashrabsn1  12553  hashfun  12607  relexpuzrel  13104  shftfn  13125  sqrlem6  13300  rlimss  13554  lo1dm  13571  o1dm  13582  rlimrege0  13631  fsumf1o  13777  fsumge0  13843  incexc2  13884  supcvg  13902  fprodf1o  13988  divalglem9  14369  divalglem9OLD  14370  bitsfzolem  14395  bitsfzolemOLD  14396  bitsinv2  14405  bitsf1ocnv  14406  bitsf1  14408  gcdcllem1  14461  bezout  14498  prmind2  14623  nprm  14626  sqnprm  14634  dvdsprm  14635  isprm5  14639  coprm  14645  phibndlem  14706  dfphi2  14710  phimullem  14715  pclem  14776  pcpre1  14780  pcidlem  14809  expnprm  14835  prmreclem1  14848  prmreclem2  14849  prmreclem5  14852  1arith  14859  4sqlem18OLD  14894  4sqlem18  14900  vdwnnlem3  14935  ramtlecl  14939  rami  14960  0ram  14966  ramub1lem1  14972  prmgaplem5  15013  firest  15319  acsfiel  15548  isacs1i  15551  catlid  15577  catrid  15578  fullfo  15805  fthf1  15810  fthoppc  15816  invfuc  15867  prslem  16164  posi  16183  dlatmjdi  16428  pslem  16440  tsrlin  16453  cnvtsr  16456  tsrdir  16472  mndid  16537  mhmf  16575  mhmlin  16577  mhm0  16578  mrcmndind  16601  grpinvex  16669  grplinv  16700  mulgz  16767  mulgdirlem  16770  mulgdir  16771  mulgass  16776  nsgbi  16836  nmzbi  16845  ghmf  16875  ghmlin  16876  conjnsg  16906  gimf1o  16915  gagrpid  16936  gaf  16937  gaass  16939  psgnunilem5  17123  odid  17175  odidOLD  17191  odf1o2  17210  gexid  17220  sylow1lem4  17241  odcau  17244  pj1id  17337  efgredeu  17390  ablcmn  17424  cmncom  17434  mulgdi  17455  gexexlem  17478  torsubg  17480  cyggenod2  17508  cygctb  17514  ghmcyg  17518  dprdf1o  17653  dprd2dlem1  17662  dprd2da  17663  ablfacrplem  17686  ablfaclem2  17707  ablfac2  17710  crngmgp  17776  rhmmhm  17938  rhmghm  17941  drngunit  17968  drngmgp  17975  drngid  17977  subrgss  17997  subrg1cl  18004  issubdrg  18021  abvge0  18041  srngcnv  18069  lmhmlin  18246  lmimf1o  18274  lvecdrng  18316  lspsolvlem  18353  islbs3  18366  lbsextlem3  18371  2idlcpbl  18446  nzrnz  18472  opprnzr  18477  rrgeq0i  18501  domneq0  18509  domnrrg  18512  drngdomn  18515  fldidom  18517  assalem  18528  mplsubrglem  18651  mplcoe1  18677  mplbas2  18682  opsrtoslem2  18696  mplelsfi  18702  coe1mul2  18850  zringunit  19049  prmirredlem  19051  znidomb  19119  cygzn  19128  psgndiflemB  19155  pjf  19263  frlmsslsp  19341  frlmlbs  19342  f1lindf  19367  pmatcoe1fsupp  19712  toponuni  19929  tpsuni  19940  clsval2  20052  mretopd  20095  neips  20116  neiptoptop  20134  neiptopnei  20135  perflp  20157  perfi  20158  restfpw  20182  cnf  20249  cnpf  20250  cnpimaex  20259  cnima  20268  t0sep  20327  t1sncld  20329  t1ficld  20330  hausnei  20331  regsep  20337  pnrmcld  20345  nrmsep3  20358  cnrmi  20363  cmpcov  20391  discmp  20400  tgcmp  20403  uncmp  20405  hauscmplem  20408  cmpfi  20410  conclo  20417  1stcclb  20446  2ndcdisj  20458  llyi  20476  nllyi  20477  ptpjpre1  20573  ptpjcn  20613  ptpjopn  20614  ptclsg  20617  dfac14  20620  txdis1cn  20637  pthaus  20640  hauseqlcld  20648  txkgen  20654  xkococn  20662  txcon  20691  hmeocnvcn  20763  fbssfi  20839  filss  20855  ufilss  20907  uffixfr  20925  flimneiss  20968  flimelbas  20970  fclscf  21027  flimfnfcls  21030  alexsublem  21046  alexsubb  21048  alexsubALT  21053  ptcmplem2  21055  ptcmplem3  21056  ptcmplem4  21057  tmdgsum2  21098  ghmcnp  21116  tgpt0  21120  qustgplem  21122  tsmsfbas  21129  tsmslem1  21130  tsmsgsum  21140  tsmssubm  21144  tsmsres  21145  tsmsf1o  21146  tsmsmhm  21147  tsmsadd  21148  tsmsxplem1  21154  tsmsxplem2  21155  tsmsxp  21156  istdrg2  21179  vscacn  21187  tvctdrg  21194  uspreg  21276  ucncn  21287  neipcfilu  21298  cuspcvg  21303  psmetxrge0  21316  isxmet2d  21329  prdsxmetlem  21370  imasdsf1olem  21375  xmstopn  21453  mstopn  21454  stdbdxmet  21517  prdsxmslem2  21531  nrgabv  21651  nmvs  21666  nvclvec  21686  nmoge0  21713  nghmcl  21719  nmoi  21720  nmoge0OLD  21731  nmoiOLD  21736  nghmghm  21742  nmhmlmhm  21757  nmhmnghm  21758  icccmp  21830  xrge0gsumle  21838  xrge0tsms  21839  metds0  21854  metdstri  21855  metdsre  21857  metdseq0  21858  metdscnlem  21859  metnrmlem1a  21862  metds0OLD  21869  metdstriOLD  21870  metdsreOLD  21872  metdseq0OLD  21873  metdscnlemOLD  21874  metnrmlem1aOLD  21877  icopnfcnv  21957  xrhmeo  21961  pcoval1  22031  cvslvec  22124  cvsunit  22126  cphreccllem  22143  cmetcvg  22242  lmle  22258  cmscmet  22301  cmetcusp1  22307  hlcph  22318  minveclem4  22361  minveclem4OLD  22373  ivthlem3  22391  ovolmge0  22417  ovolicc1  22456  ovolicc2lem3  22459  ovolicc2lem5  22462  mblsplit  22473  dyadmbl  22545  mbfdm  22571  mbfadd  22604  mbfsub  22605  i1ff  22621  i1frn  22622  i1fima2  22624  mbfmul  22671  itg2monolem1  22695  bddmulibl  22783  dvnres  22872  c1liplem1  22935  c1lip2  22937  dvge0  22945  lhop1lem  22952  itgsubstlem  22987  fta1glem1  23103  fta1glem2  23104  fta1b  23107  plyf  23139  plypf1  23153  plyadd  23158  plymul  23159  coeeu  23166  dgrlem  23170  coeid  23179  elqaalem3  23261  elqaalem3OLD  23264  aareccl  23269  eff1olem  23484  relogf1o  23503  logdmn0  23572  logcnlem2  23575  logcnlem3  23576  dvloglem  23580  efopnlem1  23588  efopnlem2  23589  logtayl2  23594  cxpcn3lem  23674  cxpcn3  23675  atandmneg  23819  atandmcj  23822  efiatan2  23830  cosatan  23834  cosatanne0  23835  dvatan  23848  areage0  23876  cxp2lim  23889  jensenlem2  23900  jensen  23901  eldmgm  23934  dmgmaddn0  23935  dmlogdmgm  23936  lgamgulmlem2  23942  lgamgulmlem3  23943  lgamgulmlem5  23945  lgambdd  23949  lgamucov  23950  wilthlem1  23980  wilth  23983  ftalem3  23986  efnnfsumcl  24016  isppw  24028  efchtdvds  24073  sqff1o  24096  dvdsdivcl  24097  fsumdvdsdiaglem  24099  dvdsppwf1o  24102  dvdsflf1o  24103  musum  24107  muinv  24109  dvdsmulf1o  24110  fsumvma2  24129  vmasum  24131  chpval2  24133  chpchtsum  24134  chpub  24135  mersenne  24142  perfect1  24143  bposlem1  24199  bposlem5  24203  lgsfle1  24220  lgsle1  24226  lgsdirprm  24244  lgsne0  24248  lgsqrlem4  24259  lgseisenlem3  24266  lgseisenlem4  24267  lgsquadlem1  24269  lgsquadlem2  24270  2sqblem  24292  chebbnd1lem1  24294  chebbnd1  24297  chtppilim  24300  chpchtlim  24304  chpo1ub  24305  rplogsumlem2  24310  rpvmasumlem  24312  dchrmusumlema  24318  dchrvmasumlem1  24320  dchrisum0flblem2  24334  dchrisum0lema  24339  dchrisum0lem2a  24342  logsqvma  24367  selberg3lem2  24383  pntrsumo1  24390  pnt2  24438  ostthlem1  24452  ostth3  24463  axtgcgrrflx  24497  axtgcgrid  24498  axtgsegcon  24499  axtg5seg  24500  axtgbtwnid  24501  axtgpasch  24502  axtgcont1  24503  tglng  24578  axcontlem7  24987  axcontlem10  24990  umgrale  25035  usgraedg2  25089  usgraexmpledg  25117  clwlkfclwwlk1hashn  25555  eupatrl  25682  gxneg  25980  gxadd  25989  gxmul  25992  ablocom  25999  subgoablo  26025  smgrpisass  26047  mndoisexid  26054  zrdivrng  26146  phpar2  26450  cbncms  26493  hlph  26527  hcaucvg  26825  hlimconvi  26830  shaddcl  26856  shmulcl  26857  chlimi  26873  chcompl  26881  choc1  26966  nmopre  27509  cnopc  27552  lnopl  27553  unop  27554  hmop  27561  cnfnc  27569  lnfnl  27570  nlelshi  27699  cnlnadjlem5  27710  elpjidm  27823  mdslle1i  27956  mdslle2i  27957  atcv0  27981  chpssati  28002  elin2d  28141  fovcld  28229  aciunf1lem  28254  padct  28301  ssnnssfz  28361  ressprs  28411  oduprs  28412  resspos  28415  resstos  28416  tleile  28417  ogrpinvOLD  28473  ogrpinv0le  28474  ogrpsub  28475  ogrpaddlt  28476  isarchi3  28499  archirng  28500  archirngz  28501  archiabllem1a  28503  archiabllem1b  28504  archiabllem2a  28506  archiabllem2c  28507  archiabllem2b  28508  archiabl  28510  orngsqr  28563  ornglmulle  28564  orngrmulle  28565  ofldtos  28570  ofldlt1  28572  ofldchr  28573  suborng  28574  subofld  28575  isarchiofld  28576  nn0omnd  28600  madjusmdetlem4  28652  qtophaus  28659  crefi  28670  cmpcref  28673  cmppcmp  28681  pcmplfin  28683  tpr2rico  28714  rge0scvg  28751  zrhunitpreima  28778  qqhrhm  28789  esummono  28871  gsumesum  28876  esumrnmpt2  28885  esumpinfval  28890  esumpcvgval  28895  esumpmono  28896  0elsiga  28932  sigaclcu  28935  issgon  28941  inelpisys  28972  ldsysgenld  28978  ldgenpisyslem1  28981  sxuni  29011  isrnmeas  29018  measvuni  29032  measssd  29033  ddemeas  29055  imambfm  29080  elmbfmvol2  29085  dya2icoseg2  29096  omssubaddlem  29123  omssubadd  29124  omssubaddlemOLD  29127  omssubaddOLD  29128  carsgsigalem  29143  pmeasmono  29153  sibfinima  29168  oddpwdc  29183  oddpwdcv  29184  eulerpartlemf  29199  eulerpartlemt  29200  eulerpartlemr  29203  eulerpartlemgvv  29205  eulerpartlemgs2  29209  sseqf  29221  fiblem  29227  probtot  29241  ballotlem4  29327  ballotlem5  29328  ballotlemfrc  29355  ballotlemirc  29360  ballotth  29366  ballotlemfrcOLD  29393  ballotlemircOLD  29398  ballotthOLD  29404  bnj642  29554  bnj643  29555  bnj645  29556  bnj707  29561  bnj1379  29638  bnj1538  29662  bnj110  29665  bnj93  29670  bnj906  29737  bnj1006  29766  bnj1110  29787  bnj1121  29790  bnj1172  29806  bnj1204  29817  bnj1321  29832  bnj1364  29833  bnj1398  29839  bnj1450  29855  bnj1312  29863  bnj1501  29872  bnj1523  29876  subfacp1lem3  29901  subfacp1lem5  29903  pconcn  29943  sconpht  29948  conpcon  29954  cvmcov  29982  cvmliftlem1  30004  cvmliftlem10  30013  cvmlift2lem11  30032  cvmlift2lem12  30033  msubff1  30190  mvhf1  30193  mthmpps  30216  mclspps  30218  fundmpss  30402  tfisg  30452  frinsg  30478  frrlem5  30513  sltval2  30538  txpss3v  30638  pprodss4v  30644  fnetg  30994  neibastop1  31008  filnetlem3  31029  onint1  31102  bj-elid2  31592  icorempt2  31695  wl-nfeqfb  31784  phpreu  31843  fin2solem  31845  fin2so  31846  ptrest  31853  poimirlem1  31855  poimirlem2  31856  poimirlem3  31857  poimirlem4  31858  poimirlem5  31859  poimirlem6  31860  poimirlem7  31861  poimirlem8  31862  poimirlem9  31863  poimirlem10  31864  poimirlem11  31865  poimirlem12  31866  poimirlem13  31867  poimirlem14  31868  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem18  31872  poimirlem19  31873  poimirlem20  31874  poimirlem21  31875  poimirlem22  31876  poimirlem23  31877  poimirlem24  31878  poimirlem25  31879  poimirlem26  31880  poimirlem27  31881  poimirlem29  31883  poimirlem31  31885  mblfinlem2  31892  dvtan  31906  itg2gt0cn  31911  ftc1anclem7  31937  ftc1anclem8  31938  ftc1anc  31939  cover2  31954  indexa  31974  istotbnd3  32017  sstotbnd2  32020  sstotbnd  32021  totbndss  32023  equivtotbnd  32024  isbnd3  32030  totbndbnd  32035  equivbnd  32036  prdsbnd  32039  prdstotbnd  32040  heibor  32067  crngocom  32148  isfld2  32152  dmncrng  32203  prter2  32371  toycom  32458  lsateln0  32480  lpssat  32498  lssat  32501  oposlem  32667  olop  32699  omllaw  32728  cvlexch1  32813  dihpN  34823  mapdordlem2  35124  nacsfg  35466  nacsfix  35473  mzpindd  35507  diophrw  35520  diophrex  35537  rexzrexnn0  35566  pell1234qrdich  35627  rmspecsqrtnq  35674  rmspecnonsq  35675  rmspecfund  35677  rmspecpos  35684  monotoddzzfi  35710  ltrmxnn0  35719  rmxnn  35721  jm2.23  35771  jm3.1lem2  35793  dnnumch3  35825  lnmlssfg  35858  lnmlmic  35866  lnrlnm  35892  lnr2i  35895  lpirlnr  35896  hbtlem6  35908  hbt  35909  mnccoe  35917  cntzsdrg  35988  idomrootle  35989  proot1mul  35993  phisum  35996  proot1hash  35997  deg1mhm  36004  radcnvrat  36521  binomcxplemdvbinom  36560  binomcxplemcvg  36561  binomcxplemnotnn0  36563  ordelordALT  36756  2uasbanh  36786  ordelordALTVD  37125  foelrnf  37311  disjinfi  37318  sumnnodd  37530  stoweidlem7  37687  stoweidlem14  37694  stoweidlem16  37696  stoweidlem24  37704  stoweidlem31  37712  stoweidlem54  37735  wallispilem3  37749  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem48  37838  fourierdlem51  37841  fourierdlem64  37854  fourierdlem76  37866  fourierdlem79  37869  fourierdlem81  37871  fourierdlem87  37877  etransclem28  37947  etransclem32  37951  sge0fodjrnlem  38046  2reu1  38320  nfunsnafv  38356  faovcl  38414  evendiv2z  38473  oddp1div2z  38474  2dvdseven  38495  2ndvdsodd  38496  perfectALTVlem1  38555  umgrle  38843  usgredg2  38907  usgra2pth  38940  clintopcllaw  39119  0ringbas  39143  rnghmmgmhm  39166  uzlidlring  39201  rnghmsubcsetclem1  39249  rngccatidALTV  39263  zrinitorngc  39274  zrtermorngc  39275  rhmsubcsetclem1  39295  funcringcsetcALTV2lem7  39316  ringccatidALTV  39326  funcringcsetclem7ALTV  39339  irinitoringc  39343  zrtermoringc  39344  fldhmsubc  39358  fldhmsubcALTV  39377  ssnn0ssfz  39404  el0ldepsnzr  39534  eluz2gt1  39579  regt1loggt0  39621  elbigodm  39640  fllogbd  39645
  Copyright terms: Public domain W3C validator