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

Theorem simprbi 464
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 194 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simprd 463 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  xornan  1368  sb1  1714  eumo  2308  2eu1OLD  2387  reurmo  3084  pssne  3605  pssn2lp  3610  ssnpss  3612  eldifn  3632  rabsnt  4110  eldifsni  4159  unimax  4287  ssintub  4306  reusv6OLD  4664  moop2  4748  pwssun  4792  weso  4876  ordwe  4897  opelxp2  5039  eldmeldmressn  5320  funmo  5610  funopg  5626  funun  5636  fununi  5660  funimaexg  5671  fndm  5686  frn  5743  f1ss  5792  f1ssr  5793  f1ssres  5794  forn  5804  f1f1orn  5833  f1orescnv  5837  f1imacnv  5838  funcocnv2  5846  dffv2  5947  exfo  6050  foelrn  6051  isorel  6221  isoini2  6234  f1ofveu  6290  fovcl  6402  f1opw  6524  onminesb  6628  onminsb  6629  tfis  6684  limomss  6700  nnlim  6708  ssnlim  6713  curry1  6887  curry2  6890  f1o2ndf1  6903  fnwelem  6910  ressuppss  6931  mpt2xopn0yelv  6953  tz7.48lem  7118  dif20el  7167  oeordi  7248  oeeulem  7262  oeeui  7263  nnawordex  7298  swoer  7351  erdisj  7371  eceqoveq  7428  mapsnconst  7476  ixpn0  7513  resixpfo  7519  boxcutc  7524  sdomnen  7556  en0  7590  en1  7594  domunsncan  7629  fodomr  7680  phplem4  7711  php3  7715  unxpdomlem3  7738  fineqvlem  7746  f1opwfi  7836  fsuppcolem  7872  fsuppco  7873  mapfienlem1  7876  mapfienlem2  7877  supub  7931  suplub  7932  ordtypelem2  7956  ordtypelem3  7957  ordtypelem6  7960  ordtypelem7  7961  wemapso2OLD  7989  wemapso2lem  7990  wdom2d  8018  brwdom3  8020  ixpiunwdom  8029  inf3lem2  8058  inf3lem6  8062  oancom  8080  infdifsn  8085  cantnfp1lem3  8111  cantnflem3  8122  cantnflem4  8123  cantnfp1lem3OLD  8137  cantnflem3OLD  8144  cantnflem4OLD  8145  cantnfOLD  8146  mapfienOLD  8150  oef1o  8153  oef1oOLD  8154  cnfcom3  8160  cnfcomlemOLD  8163  cnfcom3OLD  8168  tctr  8183  tz9.12lem3  8219  scottex  8315  cardid2  8346  infxpenlem  8403  acni3  8440  cardaleph  8482  iscard3  8486  dfac5lem4  8519  dfac5lem5  8520  kmlem1  8542  cofsmo  8661  fin4en1  8701  enfin2i  8713  fin23lem28  8732  fin23lem38  8741  isf32lem6  8750  enfin1ai  8776  isfin1-3  8778  hsmexlem2  8819  hsmexlem4  8821  domtriomlem  8834  axdc2lem  8840  axdc3lem2  8843  ac6num  8871  zorn2lem2  8889  brdom3  8918  alephval2  8959  alephreg  8969  pwcfsdom  8970  smobeth  8973  fpwwe2lem6  9025  fpwwe2lem13  9032  canthp1lem2  9043  pwfseqlem3  9050  hargch  9063  winalim2  9086  gchina  9089  inar1  9165  0npi  9272  mulclpi  9283  mulcanpi  9290  nlt1pi  9296  nqereu  9319  prcdnq  9383  prnmax  9385  ltresr2  9530  axrnegex  9551  axpre-sup  9558  1nuz2  11169  zsupss  11183  rpgt0  11243  ixxss1  11559  ixxss2  11560  ixxss12  11561  lbioo  11572  ubioo  11573  iccss2  11607  iccssico2  11610  elfzuz3  11697  uzdisj  11763  nn0disj  11800  serge0  12141  expge0  12182  expge1  12183  expaddzlem  12189  hashrabsn1  12422  hashfun  12475  shftfn  12885  sqrlem6  13060  rlimss  13304  lo1dm  13321  o1dm  13332  rlimrege0  13381  fsumf1o  13524  fsumge0  13588  incexc2  13629  supcvg  13646  divalglem9  13934  bitsfzolem  13959  bitsinv2  13968  bitsf1ocnv  13969  bitsf1  13971  gcdcllem1  14024  bezout  14055  prmind2  14103  nprm  14106  sqnprm  14114  dvdsprm  14115  coprm  14116  isprm5  14128  phibndlem  14175  dfphi2  14179  phimullem  14184  pclem  14237  pcpre1  14241  pcidlem  14270  expnprm  14296  prmreclem1  14309  prmreclem2  14310  prmreclem5  14313  1arith  14320  4sqlem18  14355  vdwnnlem3  14390  ramtlecl  14393  rami  14408  0ram  14413  ramub1lem1  14419  firest  14704  acsfiel  14925  isacs1i  14928  catlid  14954  catrid  14955  fullfo  15155  fthf1  15160  fthoppc  15166  invfuc  15217  prslem  15434  posi  15453  dlatmjdi  15697  pslem  15709  tsrlin  15722  cnvtsr  15725  tsrdir  15741  mndid  15805  mhmf  15843  mhmlin  15845  mhm0  15846  mrcmndind  15868  grpinvex  15936  grplinv  15967  mulgz  16034  mulgdirlem  16037  mulgdir  16038  mulgass  16043  nsgbi  16103  nmzbi  16112  ghmf  16142  ghmlin  16143  conjnsg  16173  gimf1o  16182  gagrpid  16203  gaf  16204  gaass  16206  psgnunilem5  16390  odid  16433  odf1o2  16464  gexid  16472  sylow1lem4  16492  odcau  16495  pj1id  16588  efgredeu  16641  ablcmn  16675  cmncom  16685  mulgdi  16706  gexexlem  16729  torsubg  16731  cyggenod2  16759  cygctb  16765  ghmcyg  16769  dprdf1o  16949  dprd2dlem1  16960  dprd2da  16961  ablfacrplem  16986  ablfaclem2  17007  ablfac2  17010  crngmgp  17076  rhmmhm  17241  rhmghm  17244  drngunit  17270  drngmgp  17277  drngid  17279  subrgss  17299  subrg1cl  17306  issubdrg  17323  abvge0  17343  srngcnv  17371  lmhmlin  17550  lmimf1o  17578  lvecdrng  17620  lspsolvlem  17657  islbs3  17670  lbsextlem3  17675  2idlcpbl  17750  nzrnz  17776  opprnzr  17781  rrgeq0i  17805  domneq0  17814  domnrrg  17817  drngdomn  17820  fldidom  17822  assalem  17833  mplsubrglem  17968  mplsubrglemOLD  17969  mplcoe1  17995  mplbas2  18002  mplbas2OLD  18003  opsrtoslem2  18017  mplelsfi  18023  mplelsfiOLD  18024  coe1mul2  18178  zringunit  18387  zrngunit  18388  prmirredlem  18390  prmirredlemOLD  18393  znidomb  18467  cygzn  18476  psgndiflemB  18503  pjf  18611  frlmsslsp  18696  frlmsslspOLD  18697  frlmlbs  18698  f1lindf  18724  pmatcoe1fsupp  19069  toponuni  19295  tpsuni  19306  clsval2  19417  mretopd  19459  neips  19480  neiptoptop  19498  neiptopnei  19499  perflp  19521  perfi  19522  restfpw  19546  cnf  19613  cnpf  19614  cnpimaex  19623  cnima  19632  t0sep  19691  t1sncld  19693  t1ficld  19694  hausnei  19695  regsep  19701  pnrmcld  19709  nrmsep3  19722  cnrmi  19727  cmpcov  19755  discmp  19764  tgcmp  19767  uncmp  19769  hauscmplem  19772  cmpfi  19774  conclo  19782  1stcclb  19811  2ndcdisj  19823  llyi  19841  nllyi  19842  ptpjpre1  19938  ptpjcn  19978  ptpjopn  19979  ptclsg  19982  dfac14  19985  txdis1cn  20002  pthaus  20005  hauseqlcld  20013  txkgen  20019  xkococn  20027  txcon  20056  hmeocnvcn  20128  fbssfi  20204  filss  20220  ufilss  20272  uffixfr  20290  flimneiss  20333  flimelbas  20335  fclscf  20392  flimfnfcls  20395  alexsublem  20410  alexsubb  20412  alexsubALT  20417  ptcmplem2  20419  ptcmplem3  20420  ptcmplem4  20421  tmdgsum2  20461  ghmcnp  20479  tgpt0  20483  qustgplem  20485  tsmsfbas  20492  tsmslem1  20493  tsmsgsum  20503  tsmsgsumOLD  20506  tsmssubm  20510  tsmsresOLD  20511  tsmsres  20512  tsmsf1o  20513  tsmsmhm  20514  tsmsadd  20515  tsmsxplem1  20521  tsmsxplem2  20522  tsmsxp  20523  istdrg2  20546  vscacn  20554  tvctdrg  20561  uspreg  20643  ucncn  20654  neipcfilu  20665  cuspcvg  20670  psmetxrge0  20683  isxmet2d  20696  prdsxmetlem  20737  imasdsf1olem  20742  xmstopn  20820  mstopn  20821  stdbdxmet  20884  prdsxmslem2  20898  nrgabv  21036  nmvs  21051  nvclvec  21071  nmoge0  21094  nghmcl  21100  nmoi  21101  nghmghm  21107  nmhmlmhm  21122  nmhmnghm  21123  icccmp  21196  xrge0gsumle  21204  xrge0tsms  21205  metds0  21220  metdstri  21221  metdsre  21223  metdseq0  21224  metdscnlem  21225  metnrmlem1a  21228  icopnfcnv  21308  xrhmeo  21312  pcoval1  21379  cvslvec  21472  cvsunit  21474  cphreccllem  21491  cmetcvg  21590  lmle  21606  cmscmet  21651  cmetcusp1OLD  21657  cmetcusp1  21658  hlcph  21670  minveclem4  21713  ivthlem3  21731  ovolmge0  21754  ovolicc1  21793  ovolicc2lem3  21796  ovolicc2lem5  21798  mblsplit  21809  dyadmbl  21875  mbfdm  21901  mbfadd  21934  mbfsub  21935  i1ff  21949  i1frn  21950  i1fima2  21952  mbfmul  21999  itg2monolem1  22023  bddmulibl  22111  dvnres  22200  c1liplem1  22263  c1lip2  22265  dvge0  22273  lhop1lem  22280  itgsubstlem  22315  fta1glem1  22432  fta1glem2  22433  fta1b  22436  plyf  22461  plypf1  22475  plyadd  22480  plymul  22481  coeeu  22488  dgrlem  22492  coeid  22501  elqaalem3  22582  aareccl  22587  eff1olem  22799  relogf1o  22818  logdmn0  22885  logcnlem2  22888  logcnlem3  22889  dvloglem  22893  efopnlem1  22901  efopnlem2  22902  logtayl2  22907  cxpcn3lem  22985  cxpcn3  22986  atandmneg  23101  atandmcj  23104  efiatan2  23112  cosatan  23116  cosatanne0  23117  dvatan  23130  areage0  23157  cxp2lim  23170  jensenlem2  23181  jensen  23182  wilthlem1  23206  wilth  23209  ftalem3  23212  efnnfsumcl  23240  isppw  23252  efchtdvds  23297  sqff1o  23320  dvdsdivcl  23321  fsumdvdsdiaglem  23323  dvdsppwf1o  23326  dvdsflf1o  23327  musum  23331  muinv  23333  dvdsmulf1o  23334  fsumvma2  23353  vmasum  23355  chpval2  23357  chpchtsum  23358  chpub  23359  mersenne  23366  perfect1  23367  bposlem1  23423  bposlem5  23427  lgsfle1  23444  lgsle1  23450  lgsdirprm  23468  lgsne0  23472  lgsqrlem4  23483  lgseisenlem3  23490  lgseisenlem4  23491  lgsquadlem1  23493  lgsquadlem2  23494  2sqblem  23516  chebbnd1lem1  23518  chebbnd1  23521  chtppilim  23524  chpchtlim  23528  chpo1ub  23529  rplogsumlem2  23534  rpvmasumlem  23536  dchrmusumlema  23542  dchrvmasumlem1  23544  dchrisum0flblem2  23558  dchrisum0lema  23563  dchrisum0lem2a  23566  logsqvma  23591  selberg3lem2  23607  pntrsumo1  23614  pnt2  23662  ostthlem1  23676  ostth3  23687  axtgcgrrflx  23723  axtgcgrid  23724  axtgsegcon  23725  axtg5seg  23726  axtgbtwnid  23727  axtgpasch  23728  axtgcont1  23729  tglng  23797  axcontlem7  24105  axcontlem10  24108  umgrale  24153  usgraedg2  24207  usgraexmpledg  24235  clwlkfclwwlk1hashn  24673  eupatrl  24800  gxneg  25099  gxadd  25108  gxmul  25111  ablocom  25118  subgoablo  25144  smgrpisass  25166  mndoisexid  25173  zrdivrng  25265  phpar2  25569  cbncms  25612  hlph  25636  hcaucvg  25934  hlimconvi  25939  shaddcl  25965  shmulcl  25966  shmulclOLD  25967  chlimi  25983  chcompl  25991  choc1  26076  nmopre  26620  cnopc  26663  lnopl  26664  unop  26665  hmop  26672  cnfnc  26680  lnfnl  26681  nlelshi  26810  cnlnadjlem5  26821  elpjidm  26934  mdslle1i  27067  mdslle2i  27068  atcv0  27092  chpssati  27113  fovcld  27309  ssnnssfz  27428  ressprs  27475  oduprs  27476  resspos  27479  resstos  27480  tleile  27481  ogrpinvOLD  27537  ogrpinv0le  27538  ogrpsub  27539  ogrpaddlt  27540  isarchi3  27563  archirng  27564  archirngz  27565  archiabllem1a  27567  archiabllem1b  27568  archiabllem2a  27570  archiabllem2c  27571  archiabllem2b  27572  archiabl  27574  xrge0tsmsd  27607  orngsqr  27626  ornglmulle  27627  orngrmulle  27628  ofldtos  27633  ofldlt1  27635  ofldchr  27636  suborng  27637  subofld  27638  isarchiofld  27639  nn0omnd  27663  qtophaus  27671  crefi  27682  cmpcref  27685  cmppcmp  27693  pcmplfin  27695  tpr2rico  27726  rge0scvg  27763  zrhunitpreima  27791  qqhrhm  27802  esummono  27898  gsumesum  27899  esumpinfval  27911  esumpcvgval  27916  esumpmono  27917  0elsiga  27946  sigaclcu  27949  issgon  27955  sxuni  27996  isrnmeas  28003  measvuni  28017  measssd  28018  ddemeas  28040  imambfm  28065  elmbfmvol2  28070  dya2icoseg2  28081  sibfinima  28113  oddpwdc  28125  oddpwdcv  28126  eulerpartlemf  28141  eulerpartlemt  28142  eulerpartlemr  28145  eulerpartlemgvv  28147  eulerpartlemgs2  28151  sseqf  28163  fiblem  28169  probtot  28183  ballotlem4  28269  ballotlem5  28270  ballotlemfrc  28297  ballotlemirc  28302  ballotth  28308  eldmgm  28396  dmgmaddn0  28397  dmlogdmgm  28398  lgamgulmlem2  28404  lgamgulmlem3  28405  lgamgulmlem5  28407  lgambdd  28411  lgamucov  28412  subfacp1lem3  28458  subfacp1lem5  28460  pconcn  28501  sconpht  28506  conpcon  28512  cvmcov  28540  cvmliftlem1  28562  cvmliftlem10  28571  cvmlift2lem11  28590  cvmlift2lem12  28591  msubff1  28748  mvhf1  28751  mthmpps  28774  mclspps  28776  fprodf1o  29012  fundmpss  29130  tfisg  29218  wfisg  29223  frinsg  29259  wfrlem5  29281  frrlem5  29325  sltval2  29350  txpss3v  29462  pprodss4v  29468  onint1  29848  wl-nfeqfb  29924  fin2solem  29973  fin2so  29974  ptrest  29982  mblfinlem2  29986  dvtan  29999  itg2gt0cn  30004  ftc1anclem7  30030  ftc1anclem8  30031  ftc1anc  30032  fnetg  30097  neibastop1  30111  filnetlem3  30132  cover2  30138  indexa  30158  istotbnd3  30201  sstotbnd2  30204  sstotbnd  30205  totbndss  30207  equivtotbnd  30208  isbnd3  30214  totbndbnd  30219  equivbnd  30220  prdsbnd  30223  prdstotbnd  30224  heibor  30251  crngocom  30332  isfld2  30336  dmncrng  30387  prter2  30556  nacsfg  30571  nacsfix  30578  mzpindd  30612  diophrw  30626  diophrex  30643  rexzrexnn0  30671  pell1234qrdich  30731  rmspecsqrtnq  30776  rmspecnonsq  30777  rmspecfund  30779  rmspecpos  30786  monotoddzzfi  30812  ltrmxnn0  30821  rmxnn  30823  jm2.23  30872  jm3.1lem2  30894  dnnumch3  30927  lnmlssfg  30960  lnmlmic  30968  lnrlnm  30996  lnr2i  30999  lpirlnr  31000  hbtlem6  31012  hbt  31013  mnccoe  31022  cntzsdrg  31086  idomrootle  31087  proot1mul  31091  phisum  31094  proot1hash  31095  deg1mhm  31102  elinel2  31332  sumnnodd  31501  icccncfext  31555  stoweidlem7  31636  stoweidlem14  31643  stoweidlem16  31645  stoweidlem24  31653  stoweidlem31  31660  stoweidlem54  31683  wallispilem3  31696  fourierdlem42  31778  fourierdlem48  31784  fourierdlem49  31785  fourierdlem51  31787  fourierdlem64  31800  fourierdlem76  31812  fourierdlem79  31815  fourierdlem81  31817  fourierdlem87  31823  2reu1  31987  nfunsnafv  32023  faovcl  32081  usgra2pth  32150  clintopcllaw  32300  uzlidlring  32335  ringccatid  32374  funcringcsetclem7  32388  fldhmsubc  32403  ssnn0ssfz  32423  el0ldepsnzr  32555  ordelordALT  32794  2uasbanh  32820  ordelordALTVD  33153  bnj642  33290  bnj643  33291  bnj645  33292  bnj707  33297  bnj1379  33374  bnj1538  33398  bnj110  33401  bnj93  33406  bnj906  33473  bnj1006  33502  bnj1110  33523  bnj1121  33526  bnj1172  33542  bnj1204  33553  bnj1321  33568  bnj1364  33569  bnj1398  33575  bnj1450  33591  bnj1312  33599  bnj1501  33608  bnj1523  33612  bj-elid2  34079  toycom  34176  lsateln0  34198  lpssat  34216  lssat  34219  oposlem  34385  olop  34417  omllaw  34446  cvlexch1  34531  dihpN  36539  mapdordlem2  36840
  Copyright terms: Public domain W3C validator