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  2910  funprg  5383  omeulem2  6668  uniinqs  6826  unxpdomlem3  7157  elfiun  7273  cofsmo  7985  isfin2-2  8035  isf32lem9  8077  tskun  8498  tskurn  8501  reclem3pr  8763  dmdcan  9560  lt2msq1  9729  supmullem1  9810  supmul  9812  xaddass2  10662  xlt2add  10672  xmulasslem3  10698  iccsplit  10860  expaddzlem  11238  expaddz  11239  expmulz  11241  limsupgle  12047  o1add  12183  o1mul  12184  o1sub  12185  bitsfzo  12723  sadfval  12740  smufval  12765  prmexpb  12893  4sqlem18  13106  vdwlem10  13134  mrieqv2d  13640  curf1  14098  spwpr4  14439  mndodcong  14956  subgabl  15231  gex2abl  15242  cntzsubr  15676  abvres  15703  lbsind2  15933  lbsextlem2  16011  lbsextg  16014  cnprest  17123  isreg2  17211  fbssfi  17634  hausflimlem  17776  tmdgsum  17880  ssbl  18073  xrsmopn  18420  dvres2  19366  vieta1  19796  aalioulem4  19819  cxpadd  20137  cxpsub  20140  divcxp  20145  cxple2  20155  cxplt2  20156  cxpcn3lem  20198  angcan  20211  ang180lem5  20222  isosctrlem3  20231  chscllem4  22333  measinblem  23838  cvmlift2lem6  24243  dedekind  24488  poseq  24811  brbtwn2  25092  axcontlem4  25154  axcontlem8  25158  linethru  25335  cnres2  25806  pellfundex  26294  congtr  26375  fzmaxdif  26391  isnumbasgrplem2  26592  matrng  26803  idomsubgmo  26837  stoweidlem31  27103  lcv1  29300  lfl1  29329  lshpkrex  29377  hlrelat3  29670  cvrval3  29671  cvrval4N  29672  athgt  29714  atcvrlln2  29777  atcvrlln  29778  lvolnle3at  29840  lvolnlelpln  29843  4atlem11  29867  4atlem12  29870  2lplnj  29878  dalemddea  29942  cdlema2N  30050  paddasslem2  30079  atmod1i1m  30116  lhp2lt  30259  lhp0lt  30261  lhpexle3lem  30269  lhpj1  30280  lhpmcvr4N  30284  lhpelim  30295  lhpmod2i2  30296  lhpmod6i1  30297  cdlemb2  30299  lhpat  30301  ltrnatb  30395  ltrnel  30397  ltrncnvel  30400  ltrncnv  30404  ltrnmw  30409  trlval2  30421  trljat1  30424  trljat2  30425  trlnidatb  30435  cdlemc1  30449  cdlemc2  30450  cdlemc5  30453  cdlemc6  30454  cdleme0aa  30468  cdleme0b  30470  cdleme0c  30471  cdleme0e  30475  cdleme0fN  30476  cdleme01N  30479  cdleme0ex1N  30481  cdleme0moN  30483  cdleme3g  30492  cdleme3h  30493  cdleme3  30495  cdleme4  30496  cdleme4a  30497  cdleme5  30498  cdleme8  30508  cdleme9  30511  cdleme10  30512  cdleme16aN  30517  cdleme11fN  30522  cdleme11g  30523  cdleme11k  30526  cdleme13  30530  cdleme17c  30546  cdleme17d1  30547  cdleme18c  30551  cdleme22gb  30552  cdlemeda  30556  cdlemednpq  30557  cdlemednuN  30558  cdleme19c  30563  cdleme20aN  30567  cdleme20bN  30568  cdleme20c  30569  cdleme22aa  30597  cdleme22d  30601  cdleme22e  30602  cdleme27cl  30624  cdleme27a  30625  cdleme30a  30636  cdleme42a  30729  cdleme42c  30730  cdlemg2fv2  30858  cdlemg2m  30862  cdlemg4g  30874  cdlemg4  30875  cdlemg6c  30878  cdlemg7aN  30883  cdlemg9a  30890  cdlemg9b  30891  cdlemg10c  30897  cdlemg12a  30901  cdlemg12b  30902  cdlemg17a  30919  cdlemg18b  30937  cdlemg18c  30938  trlcoabs2N  30980  trlcolem  30984  tendoco2  31026  tendoicl  31054  cdlemi1  31076  cdlemi2  31077  cdlemj3  31081  tendocan  31082  cdlemk3  31091  cdlemk4  31092  cdlemk5a  31093  cdlemk9  31097  cdlemk9bN  31098  cdlemk10  31101  cdlemk30  31152  cdlemk31  31154  cdlemk39  31174  cdlemkfid1N  31179  cdlemkfid2N  31181  cdlemk19ylem  31188  cdlemk19xlem  31200  cdlemk53b  31214  cdlemk53  31215  cdlemk55a  31217  cdlemk43N  31221  cdlemk19u1  31227  cdlemm10N  31377  cdlemn2  31454  cdlemn10  31465  dihjustlem  31475  dihord2cN  31480  dihvalcq2  31506  dihopelvalcpre  31507  dihord5b  31518  dihord6b  31519  dihmeetlem2N  31558  dihmeetbclemN  31563  dihmeetlem4preN  31565  dihmeetALTN  31586  dochshpncl  31643  dochsatshpb  31711  hdmapval3N  32100  hgmap11  32164
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