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

Theorem simprbi 466
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 198 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 465 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  xornan  1413  sb1  1799  eumo  2327  reurmo  3009  pssne  3528  pssn2lp  3533  ssnpss  3535  eldifn  3555  elinel2  3619  elin2d  3622  rabsnt  4048  eldifsni  4097  unimax  4232  ssintub  4251  moop2  4695  pwssun  4739  weso  4824  opelxp2  4867  eldmeldmressn  5144  wfisg  5414  ordwe  5435  funmo  5597  funopg  5613  funun  5623  fununi  5647  funimaexg  5658  fndm  5673  frn  5733  f1ss  5782  f1ssr  5783  f1ssres  5784  forn  5794  f1f1orn  5823  f1orescnv  5827  f1imacnv  5828  funcocnv2  5836  dffv2  5936  exfo  6038  foelrn  6039  isorel  6215  isoini2  6228  f1ofveu  6283  fovcl  6398  f1opw  6520  onminesb  6622  onminsb  6623  tfis  6678  limomss  6694  nnlim  6702  ssnlim  6707  curry1  6885  curry2  6888  f1o2ndf1  6901  fnwelem  6908  ressuppss  6931  mpt2xopn0yelv  6956  wfrlem5  7037  tz7.48lem  7155  dif20el  7204  oeordi  7285  oeeulem  7299  oeeui  7300  nnawordex  7335  swoer  7388  erdisj  7408  eceqoveq  7465  mapsnconst  7514  ixpn0  7551  resixpfo  7557  boxcutc  7562  sdomnen  7595  en0  7629  en1  7633  domunsncan  7669  fodomr  7720  phplem4  7751  php3  7755  unxpdomlem3  7775  fineqvlem  7783  f1opwfi  7875  fsuppcolem  7911  fsuppco  7912  mapfienlem1  7915  mapfienlem2  7916  supub  7970  suplub  7971  ordtypelem2  8031  ordtypelem3  8032  ordtypelem6  8035  ordtypelem7  8036  wemapso2lem  8064  wdom2d  8092  brwdom3  8094  ixpiunwdom  8103  inf3lem2  8131  inf3lem6  8135  oancom  8153  infdifsn  8159  cantnfp1lem3  8182  cantnflem3  8193  cantnflem4  8194  oef1o  8200  cnfcom3  8206  tctr  8221  tz9.12lem3  8257  scottex  8353  cardid2  8384  infxpenlem  8441  acni3  8475  cardaleph  8517  iscard3  8521  dfac5lem4  8554  dfac5lem5  8555  kmlem1  8577  cofsmo  8696  fin4en1  8736  enfin2i  8748  fin23lem28  8767  fin23lem38  8776  isf32lem6  8785  enfin1ai  8811  isfin1-3  8813  hsmexlem2  8854  hsmexlem4  8856  domtriomlem  8869  axdc2lem  8875  axdc3lem2  8878  ac6num  8906  zorn2lem2  8924  brdom3  8953  alephval2  8994  alephreg  9004  pwcfsdom  9005  smobeth  9008  fpwwe2lem6  9057  fpwwe2lem13  9064  canthp1lem2  9075  pwfseqlem3  9082  hargch  9095  winalim2  9118  gchina  9121  inar1  9197  0npi  9304  mulclpi  9315  mulcanpi  9322  nlt1pi  9328  nqereu  9351  prcdnq  9415  prnmax  9417  ltresr2  9562  axrnegex  9583  axpre-sup  9590  1nuz2  11231  zsupss  11250  rpgt0  11310  ixxss1  11650  ixxss2  11651  ixxss12  11652  lbioo  11664  ubioo  11665  iccss2  11702  iccssico2  11705  elfzuz3  11794  uzdisj  11864  nn0disj  11904  serge0  12264  expge0  12305  expge1  12306  expaddzlem  12312  hashrabsn1  12550  hashfun  12606  relexpuzrel  13108  shftfn  13129  sqrlem6  13304  rlimss  13559  lo1dm  13576  o1dm  13587  rlimrege0  13636  fsumf1o  13782  fsumge0  13848  incexc2  13889  supcvg  13907  fprodf1o  13993  divalglem9  14374  divalglem9OLD  14375  bitsfzolem  14400  bitsfzolemOLD  14401  bitsinv2  14410  bitsf1ocnv  14411  bitsf1  14413  gcdcllem1  14466  bezout  14503  prmind2  14628  nprm  14631  sqnprm  14639  dvdsprm  14640  isprm5  14644  coprm  14650  phibndlem  14711  dfphi2  14715  phimullem  14720  pclem  14781  pcpre1  14785  pcidlem  14814  expnprm  14840  prmreclem1  14853  prmreclem2  14854  prmreclem5  14857  1arith  14864  4sqlem18OLD  14899  4sqlem18  14905  vdwnnlem3  14940  ramtlecl  14944  rami  14965  0ram  14971  ramub1lem1  14977  prmgaplem5  15018  firest  15324  acsfiel  15553  isacs1i  15556  catlid  15582  catrid  15583  fullfo  15810  fthf1  15815  fthoppc  15821  invfuc  15872  prslem  16169  posi  16188  dlatmjdi  16433  pslem  16445  tsrlin  16458  cnvtsr  16461  tsrdir  16477  mndid  16542  mhmf  16580  mhmlin  16582  mhm0  16583  mrcmndind  16606  grpinvex  16674  grplinv  16705  mulgz  16772  mulgdirlem  16775  mulgdir  16776  mulgass  16781  nsgbi  16841  nmzbi  16850  ghmf  16880  ghmlin  16881  conjnsg  16911  gimf1o  16920  gagrpid  16941  gaf  16942  gaass  16944  psgnunilem5  17128  odid  17180  odidOLD  17196  odf1o2  17215  gexid  17225  sylow1lem4  17246  odcau  17249  pj1id  17342  efgredeu  17395  ablcmn  17429  cmncom  17439  mulgdi  17460  gexexlem  17483  torsubg  17485  cyggenod2  17513  cygctb  17519  ghmcyg  17523  dprdf1o  17658  dprd2dlem1  17667  dprd2da  17668  ablfacrplem  17691  ablfaclem2  17712  ablfac2  17715  crngmgp  17781  rhmmhm  17943  rhmghm  17946  drngunit  17973  drngmgp  17980  drngid  17982  subrgss  18002  subrg1cl  18009  issubdrg  18026  abvge0  18046  srngcnv  18074  lmhmlin  18251  lmimf1o  18279  lvecdrng  18321  lspsolvlem  18358  islbs3  18371  lbsextlem3  18376  2idlcpbl  18451  nzrnz  18477  opprnzr  18482  rrgeq0i  18506  domneq0  18514  domnrrg  18517  drngdomn  18520  fldidom  18522  assalem  18533  mplsubrglem  18656  mplcoe1  18682  mplbas2  18687  opsrtoslem2  18701  mplelsfi  18707  coe1mul2  18855  zringunit  19055  prmirredlem  19057  znidomb  19125  cygzn  19134  psgndiflemB  19161  pjf  19269  frlmsslsp  19347  frlmlbs  19348  f1lindf  19373  pmatcoe1fsupp  19718  toponuni  19935  tpsuni  19946  clsval2  20058  mretopd  20101  neips  20122  neiptoptop  20140  neiptopnei  20141  perflp  20163  perfi  20164  restfpw  20188  cnf  20255  cnpf  20256  cnpimaex  20265  cnima  20274  t0sep  20333  t1sncld  20335  t1ficld  20336  hausnei  20337  regsep  20343  pnrmcld  20351  nrmsep3  20364  cnrmi  20369  cmpcov  20397  discmp  20406  tgcmp  20409  uncmp  20411  hauscmplem  20414  cmpfi  20416  conclo  20423  1stcclb  20452  2ndcdisj  20464  llyi  20482  nllyi  20483  ptpjpre1  20579  ptpjcn  20619  ptpjopn  20620  ptclsg  20623  dfac14  20626  txdis1cn  20643  pthaus  20646  hauseqlcld  20654  txkgen  20660  xkococn  20668  txcon  20697  hmeocnvcn  20769  fbssfi  20845  filss  20861  ufilss  20913  uffixfr  20931  flimneiss  20974  flimelbas  20976  fclscf  21033  flimfnfcls  21036  alexsublem  21052  alexsubb  21054  alexsubALT  21059  ptcmplem2  21061  ptcmplem3  21062  ptcmplem4  21063  tmdgsum2  21104  ghmcnp  21122  tgpt0  21126  qustgplem  21128  tsmsfbas  21135  tsmslem1  21136  tsmsgsum  21146  tsmssubm  21150  tsmsres  21151  tsmsf1o  21152  tsmsmhm  21153  tsmsadd  21154  tsmsxplem1  21160  tsmsxplem2  21161  tsmsxp  21162  istdrg2  21185  vscacn  21193  tvctdrg  21200  uspreg  21282  ucncn  21293  neipcfilu  21304  cuspcvg  21309  psmetxrge0  21322  isxmet2d  21335  prdsxmetlem  21376  imasdsf1olem  21381  xmstopn  21459  mstopn  21460  stdbdxmet  21523  prdsxmslem2  21537  nrgabv  21657  nmvs  21672  nvclvec  21692  nmoge0  21719  nghmcl  21725  nmoi  21726  nmoge0OLD  21737  nmoiOLD  21742  nghmghm  21748  nmhmlmhm  21763  nmhmnghm  21764  icccmp  21836  xrge0gsumle  21844  xrge0tsms  21845  metds0  21860  metdstri  21861  metdsre  21863  metdseq0  21864  metdscnlem  21865  metnrmlem1a  21868  metds0OLD  21875  metdstriOLD  21876  metdsreOLD  21878  metdseq0OLD  21879  metdscnlemOLD  21880  metnrmlem1aOLD  21883  icopnfcnv  21963  xrhmeo  21967  pcoval1  22037  cvslvec  22130  cvsunit  22132  cphreccllem  22149  cmetcvg  22248  lmle  22264  cmscmet  22307  cmetcusp1  22313  hlcph  22324  minveclem4  22367  minveclem4OLD  22379  ivthlem3  22397  ovolmge0  22423  ovolicc1  22462  ovolicc2lem3  22465  ovolicc2lem5  22468  mblsplit  22479  dyadmbl  22551  mbfdm  22577  mbfadd  22610  mbfsub  22611  i1ff  22627  i1frn  22628  i1fima2  22630  mbfmul  22677  itg2monolem1  22701  bddmulibl  22789  dvnres  22878  c1liplem1  22941  c1lip2  22943  dvge0  22951  lhop1lem  22958  itgsubstlem  22993  fta1glem1  23109  fta1glem2  23110  fta1b  23113  plyf  23145  plypf1  23159  plyadd  23164  plymul  23165  coeeu  23172  dgrlem  23176  coeid  23185  elqaalem3  23267  elqaalem3OLD  23270  aareccl  23275  eff1olem  23490  relogf1o  23509  logdmn0  23578  logcnlem2  23581  logcnlem3  23582  dvloglem  23586  efopnlem1  23594  efopnlem2  23595  logtayl2  23600  cxpcn3lem  23680  cxpcn3  23681  atandmneg  23825  atandmcj  23828  efiatan2  23836  cosatan  23840  cosatanne0  23841  dvatan  23854  areage0  23882  cxp2lim  23895  jensenlem2  23906  jensen  23907  eldmgm  23940  dmgmaddn0  23941  dmlogdmgm  23942  lgamgulmlem2  23948  lgamgulmlem3  23949  lgamgulmlem5  23951  lgambdd  23955  lgamucov  23956  wilthlem1  23986  wilth  23989  ftalem3  23992  efnnfsumcl  24022  isppw  24034  efchtdvds  24079  sqff1o  24102  dvdsdivcl  24103  fsumdvdsdiaglem  24105  dvdsppwf1o  24108  dvdsflf1o  24109  musum  24113  muinv  24115  dvdsmulf1o  24116  fsumvma2  24135  vmasum  24137  chpval2  24139  chpchtsum  24140  chpub  24141  mersenne  24148  perfect1  24149  bposlem1  24205  bposlem5  24209  lgsfle1  24226  lgsle1  24232  lgsdirprm  24250  lgsne0  24254  lgsqrlem4  24265  lgseisenlem3  24272  lgseisenlem4  24273  lgsquadlem1  24275  lgsquadlem2  24276  2sqblem  24298  chebbnd1lem1  24300  chebbnd1  24303  chtppilim  24306  chpchtlim  24310  chpo1ub  24311  rplogsumlem2  24316  rpvmasumlem  24318  dchrmusumlema  24324  dchrvmasumlem1  24326  dchrisum0flblem2  24340  dchrisum0lema  24345  dchrisum0lem2a  24348  logsqvma  24373  selberg3lem2  24389  pntrsumo1  24396  pnt2  24444  ostthlem1  24458  ostth3  24469  axtgcgrrflx  24503  axtgcgrid  24504  axtgsegcon  24505  axtg5seg  24506  axtgbtwnid  24507  axtgpasch  24508  axtgcont1  24509  tglng  24584  axcontlem7  24993  axcontlem10  24996  umgrale  25041  usgraedg2  25095  usgraexmpledg  25124  clwlkfclwwlk1hashn  25562  eupatrl  25689  gxneg  25987  gxadd  25996  gxmul  25999  ablocom  26006  subgoablo  26032  smgrpisass  26054  mndoisexid  26061  zrdivrng  26153  phpar2  26457  cbncms  26500  hlph  26534  hcaucvg  26832  hlimconvi  26837  shaddcl  26863  shmulcl  26864  chlimi  26880  chcompl  26888  choc1  26973  nmopre  27516  cnopc  27559  lnopl  27560  unop  27561  hmop  27568  cnfnc  27576  lnfnl  27577  nlelshi  27706  cnlnadjlem5  27717  elpjidm  27830  mdslle1i  27963  mdslle2i  27964  atcv0  27988  chpssati  28009  fovcld  28232  aciunf1lem  28257  padct  28300  ssnnssfz  28360  ressprs  28409  oduprs  28410  resspos  28413  resstos  28414  tleile  28415  ogrpinvOLD  28471  ogrpinv0le  28472  ogrpsub  28473  ogrpaddlt  28474  isarchi3  28497  archirng  28498  archirngz  28499  archiabllem1a  28501  archiabllem1b  28502  archiabllem2a  28504  archiabllem2c  28505  archiabllem2b  28506  archiabl  28508  orngsqr  28560  ornglmulle  28561  orngrmulle  28562  ofldtos  28567  ofldlt1  28569  ofldchr  28570  suborng  28571  subofld  28572  isarchiofld  28573  nn0omnd  28597  madjusmdetlem4  28649  qtophaus  28656  crefi  28667  cmpcref  28670  cmppcmp  28678  pcmplfin  28680  tpr2rico  28711  rge0scvg  28748  zrhunitpreima  28775  qqhrhm  28786  esummono  28868  gsumesum  28873  esumrnmpt2  28882  esumpinfval  28887  esumpcvgval  28892  esumpmono  28893  0elsiga  28929  sigaclcu  28932  issgon  28938  inelpisys  28969  ldsysgenld  28975  ldgenpisyslem1  28978  sxuni  29008  isrnmeas  29015  measvuni  29029  measssd  29030  ddemeas  29052  imambfm  29077  elmbfmvol2  29082  dya2icoseg2  29093  omssubaddlem  29120  omssubadd  29121  omssubaddlemOLD  29124  omssubaddOLD  29125  carsgsigalem  29140  pmeasmono  29150  sibfinima  29165  oddpwdc  29180  oddpwdcv  29181  eulerpartlemf  29196  eulerpartlemt  29197  eulerpartlemr  29200  eulerpartlemgvv  29202  eulerpartlemgs2  29206  sseqf  29218  fiblem  29224  probtot  29238  ballotlem4  29324  ballotlem5  29325  ballotlemfrc  29352  ballotlemirc  29357  ballotth  29363  ballotlemfrcOLD  29390  ballotlemircOLD  29395  ballotthOLD  29401  bnj642  29551  bnj643  29552  bnj645  29553  bnj707  29558  bnj1379  29635  bnj1538  29659  bnj110  29662  bnj93  29667  bnj906  29734  bnj1006  29763  bnj1110  29784  bnj1121  29787  bnj1172  29803  bnj1204  29814  bnj1321  29829  bnj1364  29830  bnj1398  29836  bnj1450  29852  bnj1312  29860  bnj1501  29869  bnj1523  29873  subfacp1lem3  29898  subfacp1lem5  29900  pconcn  29940  sconpht  29945  conpcon  29951  cvmcov  29979  cvmliftlem1  30001  cvmliftlem10  30010  cvmlift2lem11  30029  cvmlift2lem12  30030  msubff1  30187  mvhf1  30190  mthmpps  30213  mclspps  30215  fundmpss  30400  tfisg  30450  frinsg  30476  frrlem5  30511  sltval2  30536  txpss3v  30638  pprodss4v  30644  fnetg  30994  neibastop1  31008  filnetlem3  31029  onint1  31102  bj-elid2  31634  icorempt2  31747  wl-nfeqfb  31863  phpreu  31922  fin2solem  31924  fin2so  31925  ptrest  31932  poimirlem1  31934  poimirlem2  31935  poimirlem3  31936  poimirlem4  31937  poimirlem5  31938  poimirlem6  31939  poimirlem7  31940  poimirlem8  31941  poimirlem9  31942  poimirlem10  31943  poimirlem11  31944  poimirlem12  31945  poimirlem13  31946  poimirlem14  31947  poimirlem15  31948  poimirlem16  31949  poimirlem17  31950  poimirlem18  31951  poimirlem19  31952  poimirlem20  31953  poimirlem21  31954  poimirlem22  31955  poimirlem23  31956  poimirlem24  31957  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem29  31962  poimirlem31  31964  mblfinlem2  31971  dvtan  31985  itg2gt0cn  31990  ftc1anclem7  32016  ftc1anclem8  32017  ftc1anc  32018  cover2  32033  indexa  32053  istotbnd3  32096  sstotbnd2  32099  sstotbnd  32100  totbndss  32102  equivtotbnd  32103  isbnd3  32109  totbndbnd  32114  equivbnd  32115  prdsbnd  32118  prdstotbnd  32119  heibor  32146  crngocom  32227  isfld2  32231  dmncrng  32282  prter2  32447  toycom  32533  lsateln0  32555  lpssat  32573  lssat  32576  oposlem  32742  olop  32774  omllaw  32803  cvlexch1  32888  dihpN  34898  mapdordlem2  35199  nacsfg  35541  nacsfix  35548  mzpindd  35582  diophrw  35595  diophrex  35612  rexzrexnn0  35641  pell1234qrdich  35701  rmspecsqrtnq  35748  rmspecnonsq  35749  rmspecfund  35751  rmspecpos  35758  monotoddzzfi  35784  ltrmxnn0  35793  rmxnn  35795  jm2.23  35845  jm3.1lem2  35867  dnnumch3  35899  lnmlssfg  35932  lnmlmic  35940  lnrlnm  35966  lnr2i  35969  lpirlnr  35970  hbtlem6  35982  hbt  35983  mnccoe  35991  cntzsdrg  36062  idomrootle  36063  proot1mul  36067  phisum  36070  proot1hash  36071  deg1mhm  36078  radcnvrat  36657  binomcxplemdvbinom  36696  binomcxplemcvg  36697  binomcxplemnotnn0  36699  ordelordALT  36892  2uasbanh  36922  ordelordALTVD  37258  foelrnf  37455  disjinfi  37462  sumnnodd  37704  stoweidlem7  37861  stoweidlem14  37868  stoweidlem16  37870  stoweidlem24  37878  stoweidlem31  37886  stoweidlem54  37909  wallispilem3  37923  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem48  38012  fourierdlem51  38015  fourierdlem64  38028  fourierdlem76  38040  fourierdlem79  38043  fourierdlem81  38045  fourierdlem87  38051  etransclem28  38121  etransclem32  38125  sge0fodjrnlem  38252  hoidmvlelem3  38413  2reu1  38601  nfunsnafv  38638  faovcl  38696  evendiv2z  38755  oddp1div2z  38756  2dvdseven  38777  2ndvdsodd  38778  perfectALTVlem1  38837  upgrle  39168  umgredg2  39176  usgredg2ALT  39262  usgrexmpledg  39317  upgrres1  39363  fusgrvtxfi  39369  nbfusgrlevtxm1  39434  nbfusgrlevtxm2  39435  uvtxanm1nbgr  39460  cusgrcplgr  39471  usgra2pth  39655  clintopcllaw  39834  0ringbas  39858  rnghmmgmhm  39881  uzlidlring  39916  rnghmsubcsetclem1  39964  rngccatidALTV  39978  zrinitorngc  39989  zrtermorngc  39990  rhmsubcsetclem1  40010  funcringcsetcALTV2lem7  40031  ringccatidALTV  40041  funcringcsetclem7ALTV  40054  irinitoringc  40058  zrtermoringc  40059  fldhmsubc  40073  fldhmsubcALTV  40092  ssnn0ssfz  40117  el0ldepsnzr  40247  eluz2gt1  40292  regt1loggt0  40334  elbigodm  40353  fllogbd  40358
  Copyright terms: Public domain W3C validator