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

Theorem simp1r 980
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 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl1r  1007  simpr1r  1013  simp11r  1067  simp21r  1073  simp31r  1079  vtoclgft  2836  funprg  5303  omeulem2  6583  unxpdomlem3  7071  elfiun  7185  cofsmo  7897  isfin2-2  7947  isf32lem9  7989  tskun  8410  tskurn  8413  reclem3pr  8675  dmdcan  9472  lt2msq1  9641  supmullem1  9722  supmul  9724  xaddass2  10572  xlt2add  10582  xmulasslem3  10608  iccsplit  10770  expaddzlem  11147  expaddz  11148  expmulz  11150  limsupgle  11953  o1add  12089  o1mul  12090  o1sub  12091  bitsfzo  12628  sadfval  12645  smufval  12670  prmexpb  12798  4sqlem18  13011  vdwlem10  13039  mrieqv2d  13543  curf1  14001  spwpr4  14342  mndodcong  14859  subgabl  15134  gex2abl  15145  cntzsubr  15579  abvres  15606  lbsind2  15836  lbsextlem2  15914  lbsextg  15917  cnprest  17019  isreg2  17107  fbssfi  17534  hausflimlem  17676  tmdgsum  17780  ssbl  17973  xrsmopn  18320  dvres2  19264  vieta1  19694  aalioulem4  19717  cxpadd  20028  cxpsub  20031  divcxp  20036  cxple2  20046  cxplt2  20047  cxpcn3lem  20089  angcan  20102  ang180lem5  20113  isosctrlem3  20122  chscllem4  22221  measinblem  23549  cvmlift2lem6  23841  dedekind  24084  poseq  24255  brbtwn2  24535  axcontlem4  24597  axcontlem8  24601  linethru  24778  uninqs  25050  truni3  25518  intopcoaconlem3b  25549  prdnei  25584  islimrs  25591  fnctartar  25918  fnctartar2  25919  cnres2  26494  pellfundex  26982  congtr  27063  fzmaxdif  27079  isnumbasgrplem2  27280  matrng  27491  idomsubgmo  27525  stoweidlem31  27791  lcv1  29304  lfl1  29333  lshpkrex  29381  hlrelat3  29674  cvrval3  29675  cvrval4N  29676  athgt  29718  atcvrlln2  29781  atcvrlln  29782  lvolnle3at  29844  lvolnlelpln  29847  4atlem11  29871  4atlem12  29874  2lplnj  29882  dalemddea  29946  cdlema2N  30054  paddasslem2  30083  atmod1i1m  30120  lhp2lt  30263  lhp0lt  30265  lhpexle3lem  30273  lhpj1  30284  lhpmcvr4N  30288  lhpelim  30299  lhpmod2i2  30300  lhpmod6i1  30301  cdlemb2  30303  lhpat  30305  ltrnatb  30399  ltrnel  30401  ltrncnvel  30404  ltrncnv  30408  ltrnmw  30413  trlval2  30425  trljat1  30428  trljat2  30429  trlnidatb  30439  cdlemc1  30453  cdlemc2  30454  cdlemc5  30457  cdlemc6  30458  cdleme0aa  30472  cdleme0b  30474  cdleme0c  30475  cdleme0e  30479  cdleme0fN  30480  cdleme01N  30483  cdleme0ex1N  30485  cdleme0moN  30487  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4  30500  cdleme4a  30501  cdleme5  30502  cdleme8  30512  cdleme9  30515  cdleme10  30516  cdleme16aN  30521  cdleme11fN  30526  cdleme11g  30527  cdleme11k  30530  cdleme13  30534  cdleme17c  30550  cdleme17d1  30551  cdleme18c  30555  cdleme22gb  30556  cdlemeda  30560  cdlemednpq  30561  cdlemednuN  30562  cdleme19c  30567  cdleme20aN  30571  cdleme20bN  30572  cdleme20c  30573  cdleme22aa  30601  cdleme22d  30605  cdleme22e  30606  cdleme27cl  30628  cdleme27a  30629  cdleme30a  30640  cdleme42a  30733  cdleme42c  30734  cdlemg2fv2  30862  cdlemg2m  30866  cdlemg4g  30878  cdlemg4  30879  cdlemg6c  30882  cdlemg7aN  30887  cdlemg9a  30894  cdlemg9b  30895  cdlemg10c  30901  cdlemg12a  30905  cdlemg12b  30906  cdlemg17a  30923  cdlemg18b  30941  cdlemg18c  30942  trlcoabs2N  30984  trlcolem  30988  tendoco2  31030  tendoicl  31058  cdlemi1  31080  cdlemi2  31081  cdlemj3  31085  tendocan  31086  cdlemk3  31095  cdlemk4  31096  cdlemk5a  31097  cdlemk9  31101  cdlemk9bN  31102  cdlemk10  31105  cdlemk30  31156  cdlemk31  31158  cdlemk39  31178  cdlemkfid1N  31183  cdlemkfid2N  31185  cdlemk19ylem  31192  cdlemk19xlem  31204  cdlemk53b  31218  cdlemk53  31219  cdlemk55a  31221  cdlemk43N  31225  cdlemk19u1  31231  cdlemm10N  31381  cdlemn2  31458  cdlemn10  31469  dihjustlem  31479  dihord2cN  31484  dihvalcq2  31510  dihopelvalcpre  31511  dihord5b  31522  dihord6b  31523  dihmeetlem2N  31562  dihmeetbclemN  31567  dihmeetlem4preN  31569  dihmeetALTN  31590  dochshpncl  31647  dochsatshpb  31715  hdmapval3N  32104  hgmap11  32168
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator