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

Theorem simprlr 764
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprlr  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 727 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  disjxiun  4434  fcof1  6175  fliftfun  6195  domunfican  7795  finsschain  7829  suppeqfsuppbi  7845  fsuppunbi  7852  wemapsolem  7978  wemapso  7979  wemapso2OLD  7980  wemapso2lem  7981  cantnf  8115  cantnfOLD  8137  enfin2i  8704  ttukeylem7  8898  fpwwe2lem2  9013  fpwwe2lem9  9019  fpwwe2lem12  9022  fpwwelem  9026  distrlem4pr  9407  mulcmpblnr  9451  prsrlem1  9452  addsrmo  9453  mulsrmo  9454  divdivdiv  10252  divsubdiv  10267  lediv12a  10445  xmullem  11466  xlemul1a  11490  seqcaopr  12125  leexp2r  12204  hashf1lem1  12485  hashf1lem2  12486  brfi1uzind  12513  wrd2ind  12684  cshweqrep  12770  summolem2  13519  summo  13520  prodmolem2  13723  prodmo  13724  bezoutlem3  14159  bezoutlem4  14160  qredeu  14229  pcadd  14389  vdwlem9  14488  vdwlem10  14489  ramub1lem2  14526  ramub1  14527  cofucl  15235  setcmon  15392  poslubmo  15754  posglbmo  15755  grprcan  16061  isnsg3  16213  ghmpreima  16266  gaorber  16324  psgneu  16509  odcau  16602  lsmsubm  16651  lsmmod  16671  efgsfo  16735  ablfaclem3  17116  ringpropd  17208  islmodd  17496  lmodprop2d  17550  lss1d  17587  assamulgscmlem2  17976  mplcoe1  18105  mplcoe5  18109  mplcoe2OLD  18111  evlslem1  18162  lindff1  18832  islindf4  18850  mdetunilem7  19097  mdetunilem8  19098  mdetunilem9  19099  mdetuni0  19100  mdetmul  19102  ppttop  19485  epttop  19487  cnhaus  19832  isreg2  19855  cncmp  19869  1stcfb  19923  2ndcomap  19936  cldllycmp  19973  txcls  20082  ptclsg  20093  ptcnp  20100  txdis1cn  20113  txlly  20114  txnlly  20115  pthaus  20116  txhaus  20125  txkgen  20130  xkohaus  20131  xkococnlem  20137  xkococn  20138  fgabs  20357  rnelfm  20431  hausflimi  20458  hausflim  20459  alexsubALTlem2  20525  alexsubALTlem4  20527  alexsubALT  20528  tgpconcomp  20588  qustgplem  20596  metequiv2  20990  met2ndci  21002  nrmmetd  21072  nlmvscnlem1  21172  reconn  21310  xrge0tsms  21316  ipcnlem1  21662  minveclem3  21821  pmltpc  21839  ovolicc2lem5  21909  ovolicc2  21910  uniioombllem6  21974  dyadmbllem  21985  vitalilem3  21996  mbfmullem  22109  itg2split  22133  itg2mono  22137  dvlip2  22373  lhop1  22392  dvcnvrelem1  22395  ftc1lem6  22419  itgsubst  22427  dgrco  22648  plyexmo  22685  ulmdvlem3  22773  abelthlem2  22803  abelthlem8  22810  dvdsmulf1o  23446  chpchtsum  23470  dchrptlem2  23516  2sqlem5  23619  2sqlem9  23624  2sqb  23629  pntrlog2bnd  23745  pntibndlem3  23753  pntlemp  23771  pnt3  23773  mirreu3  24011  axsegcon  24206  ax5seglem9  24216  axeuclid  24242  axcontlem12  24254  clwwlkf1  24772  wwlkext2clwwlk  24779  frgranbnb  24996  ablo4  25265  ghgrpOLD  25346  smcnlem  25583  pjhthmo  26196  pjpjpre  26313  3oalem2  26557  lnconi  26928  atom1d  27248  resf1o  27529  xrge0tsmsd  27752  ballotlemfc0  28408  ballotlemfcc  28409  pconcon  28653  cvmfolem  28701  cvmliftmo  28706  cvmliftlem7  28713  cvmlift2lem10  28734  cvmlift3lem8  28748  lineext  29701  linecgr  29706  btwnconn1lem10  29721  btwnconn1lem11  29722  btwnconn3  29728  brsegle  29733  seglecgr12im  29735  segleantisym  29740  outsideoftr  29754  outsideofeq  29755  outsideofeu  29756  linethru  29778  mblfinlem3  30028  bddiblnc  30060  ftc1cnnc  30064  finminlem  30111  neibastop2lem  30153  isbnd3  30255  heibor1lem  30280  crngm4  30375  mzpcl2  30637  mzpmfp  30654  mzpmfpOLD  30655  mzpcompact2lem  30659  diophin  30681  pell14qrmulcl  30774  hbtlem2  31048  stoweidlem61  31732  fourierdlem92  31870  snlindsntor  32807  cvlcvr1  34804  4atlem12  35076  paddasslem12  35295  paddasslem13  35296  lhpexle2lem  35473  trlord  36035  cdlemkid4  36400  dihopelvalcpre  36715  dihmeetlem1N  36757  dihglblem5apreN  36758  dihmeetlem6  36776  dih1dimatlem0  36795  dihjatcclem4  36888
  Copyright terms: Public domain W3C validator