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

Theorem simp1r 1013
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1r  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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  df-3an 967
This theorem is referenced by:  simpl1r  1040  simpr1r  1046  simp11r  1100  simp21r  1106  simp31r  1112  vtoclgft  3032  funprg  5479  omeulem2  7034  uniinqs  7192  unxpdomlem3  7531  elfiun  7692  cofsmo  8450  isfin2-2  8500  isf32lem9  8542  tskun  8965  tskurn  8968  reclem3pr  9230  dedekind  9545  dmdcan  10053  lt2msq1  10227  supmullem1  10308  supmul  10310  xaddass2  11225  xlt2add  11235  xmulasslem3  11261  iccsplit  11430  expaddzlem  11919  expaddz  11920  expmulz  11922  limsupgle  12967  o1add  13103  o1mul  13104  o1sub  13105  bitsfzo  13643  sadfval  13660  smufval  13685  prmexpb  13815  4sqlem18  14035  vdwlem10  14063  mrieqv2d  14589  curf1  15047  mndodcong  16057  subgabl  16332  gex2abl  16345  cntzsubr  16909  abvres  16936  lbsind2  17174  lbsextlem2  17252  lbsextg  17255  matrng  18342  mdetunilem8  18437  maducoeval  18457  maducoeval2  18458  madurid  18462  cramerimplem3  18503  cnprest  18905  isreg2  18993  fbssfi  19422  hausflimlem  19564  tmdgsum  19678  ssblps  20009  ssbl  20010  xrsmopn  20401  dvres2  21399  vieta1  21790  aalioulem4  21813  cxpadd  22136  cxpsub  22139  divcxp  22144  cxple2  22154  cxplt2  22155  cxpcn3lem  22197  angcan  22210  ang180lem5  22221  isosctrlem3  22230  brbtwn2  23163  axcontlem4  23225  axcontlem8  23229  chscllem4  25055  ogrpinvlt  26199  pstmval  26334  measinblem  26646  cvmlift2lem6  27209  poseq  27726  linethru  28196  cnres2  28674  pellfundex  29239  congtr  29320  fzmaxdif  29336  isnumbasgrplem2  29472  idomsubgmo  29575  stoweidlem31  29838  clwwlknimp  30451  domnmsuppn0  30794  mndpfsupp  30802  lincext3  31002  lcv1  32698  lfl1  32727  lshpkrex  32775  hlrelat3  33068  cvrval3  33069  cvrval4N  33070  athgt  33112  atcvrlln2  33175  atcvrlln  33176  lvolnle3at  33238  lvolnlelpln  33241  4atlem11  33265  4atlem12  33268  2lplnj  33276  dalemddea  33340  cdlema2N  33448  paddasslem2  33477  atmod1i1m  33514  lhp2lt  33657  lhp0lt  33659  lhpexle3lem  33667  lhpj1  33678  lhpmcvr4N  33682  lhpelim  33693  lhpmod2i2  33694  lhpmod6i1  33695  cdlemb2  33697  lhpat  33699  ltrnatb  33793  ltrnel  33795  ltrncnvel  33798  ltrncnv  33802  ltrnmw  33807  trlval2  33819  trljat1  33822  trljat2  33823  trlnidatb  33833  cdlemc1  33847  cdlemc2  33848  cdlemc5  33851  cdlemc6  33852  cdleme0aa  33866  cdleme0b  33868  cdleme0c  33869  cdleme0e  33873  cdleme0fN  33874  cdleme01N  33877  cdleme0ex1N  33879  cdleme0moN  33881  cdleme3g  33890  cdleme3h  33891  cdleme3  33893  cdleme4  33894  cdleme4a  33895  cdleme5  33896  cdleme8  33906  cdleme9  33909  cdleme10  33910  cdleme16aN  33915  cdleme11fN  33920  cdleme11g  33921  cdleme11k  33924  cdleme13  33928  cdleme17c  33944  cdleme17d1  33945  cdleme18c  33949  cdleme22gb  33950  cdlemeda  33954  cdlemednpq  33955  cdlemednuN  33956  cdleme19c  33961  cdleme20aN  33965  cdleme20bN  33966  cdleme20c  33967  cdleme22aa  33995  cdleme22d  33999  cdleme22e  34000  cdleme27cl  34022  cdleme27a  34023  cdleme30a  34034  cdleme42a  34127  cdleme42c  34128  cdlemg2fv2  34256  cdlemg2m  34260  cdlemg4g  34272  cdlemg4  34273  cdlemg6c  34276  cdlemg7aN  34281  cdlemg9a  34288  cdlemg9b  34289  cdlemg10c  34295  cdlemg12a  34299  cdlemg12b  34300  cdlemg17a  34317  cdlemg18b  34335  cdlemg18c  34336  trlcoabs2N  34378  trlcolem  34382  tendoco2  34424  tendoicl  34452  cdlemi1  34474  cdlemi2  34475  cdlemj3  34479  tendocan  34480  cdlemk3  34489  cdlemk4  34490  cdlemk5a  34491  cdlemk9  34495  cdlemk9bN  34496  cdlemk10  34499  cdlemk30  34550  cdlemk31  34552  cdlemk39  34572  cdlemkfid1N  34577  cdlemkfid2N  34579  cdlemk19ylem  34586  cdlemk19xlem  34598  cdlemk53b  34612  cdlemk53  34613  cdlemk55a  34615  cdlemk43N  34619  cdlemk19u1  34625  cdlemm10N  34775  cdlemn2  34852  cdlemn10  34863  dihjustlem  34873  dihord2cN  34878  dihvalcq2  34904  dihopelvalcpre  34905  dihord5b  34916  dihord6b  34917  dihmeetlem2N  34956  dihmeetbclemN  34961  dihmeetlem4preN  34963  dihmeetALTN  34984  dochshpncl  35041  dochsatshpb  35109  hdmapval3N  35498  hgmap11  35562
  Copyright terms: Public domain W3C validator