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  2835  funprg  5267  omeulem2  6577  unxpdomlem3  7065  elfiun  7179  cofsmo  7891  isfin2-2  7941  isf32lem9  7983  tskun  8404  tskurn  8407  reclem3pr  8669  dmdcan  9466  lt2msq1  9635  supmullem1  9716  supmul  9718  xaddass2  10566  xlt2add  10576  xmulasslem3  10602  iccsplit  10764  expaddzlem  11141  expaddz  11142  expmulz  11144  limsupgle  11947  o1add  12083  o1mul  12084  o1sub  12085  bitsfzo  12622  sadfval  12639  smufval  12664  prmexpb  12792  4sqlem18  13005  vdwlem10  13033  mrieqv2d  13537  curf1  13995  spwpr4  14336  mndodcong  14853  subgabl  15128  gex2abl  15139  cntzsubr  15573  abvres  15600  lbsind2  15830  lbsextlem2  15908  lbsextg  15911  cnprest  17013  isreg2  17101  fbssfi  17528  hausflimlem  17670  tmdgsum  17774  ssbl  17967  xrsmopn  18314  dvres2  19258  vieta1  19688  aalioulem4  19711  cxpadd  20022  cxpsub  20025  divcxp  20030  cxple2  20040  cxplt2  20041  cxpcn3lem  20083  angcan  20096  ang180lem5  20107  isosctrlem3  20116  chscllem4  22215  cvmlift2lem6  23246  dedekind  23488  poseq  23657  brbtwn2  23943  axcontlem4  24005  axcontlem8  24009  linethru  24186  uninqs  24449  truni3  24918  intopcoaconlem3b  24949  prdnei  24984  islimrs  24991  fnctartar  25318  fnctartar2  25319  cnres2  25894  pellfundex  26382  congtr  26463  fzmaxdif  26479  isnumbasgrplem2  26680  matrng  26891  idomsubgmo  26925  stoweidlem31  27191  lcv1  28510  lfl1  28539  lshpkrex  28587  hlrelat3  28880  cvrval3  28881  cvrval4N  28882  athgt  28924  atcvrlln2  28987  atcvrlln  28988  lvolnle3at  29050  lvolnlelpln  29053  4atlem11  29077  4atlem12  29080  2lplnj  29088  dalemddea  29152  cdlema2N  29260  paddasslem2  29289  atmod1i1m  29326  lhp2lt  29469  lhp0lt  29471  lhpexle3lem  29479  lhpj1  29490  lhpmcvr4N  29494  lhpelim  29505  lhpmod2i2  29506  lhpmod6i1  29507  cdlemb2  29509  lhpat  29511  ltrnatb  29605  ltrnel  29607  ltrncnvel  29610  ltrncnv  29614  ltrnmw  29619  trlval2  29631  trljat1  29634  trljat2  29635  trlnidatb  29645  cdlemc1  29659  cdlemc2  29660  cdlemc5  29663  cdlemc6  29664  cdleme0aa  29678  cdleme0b  29680  cdleme0c  29681  cdleme0e  29685  cdleme0fN  29686  cdleme01N  29689  cdleme0ex1N  29691  cdleme0moN  29693  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme4a  29707  cdleme5  29708  cdleme8  29718  cdleme9  29721  cdleme10  29722  cdleme16aN  29727  cdleme11fN  29732  cdleme11g  29733  cdleme11k  29736  cdleme13  29740  cdleme17c  29756  cdleme17d1  29757  cdleme18c  29761  cdleme22gb  29762  cdlemeda  29766  cdlemednpq  29767  cdlemednuN  29768  cdleme19c  29773  cdleme20aN  29777  cdleme20bN  29778  cdleme20c  29779  cdleme22aa  29807  cdleme22d  29811  cdleme22e  29812  cdleme27cl  29834  cdleme27a  29835  cdleme30a  29846  cdleme42a  29939  cdleme42c  29940  cdlemg2fv2  30068  cdlemg2m  30072  cdlemg4g  30084  cdlemg4  30085  cdlemg6c  30088  cdlemg7aN  30093  cdlemg9a  30100  cdlemg9b  30101  cdlemg10c  30107  cdlemg12a  30111  cdlemg12b  30112  cdlemg17a  30129  cdlemg18b  30147  cdlemg18c  30148  trlcoabs2N  30190  trlcolem  30194  tendoco2  30236  tendoicl  30264  cdlemi1  30286  cdlemi2  30287  cdlemj3  30291  tendocan  30292  cdlemk3  30301  cdlemk4  30302  cdlemk5a  30303  cdlemk9  30307  cdlemk9bN  30308  cdlemk10  30311  cdlemk30  30362  cdlemk31  30364  cdlemk39  30384  cdlemkfid1N  30389  cdlemkfid2N  30391  cdlemk19ylem  30398  cdlemk19xlem  30410  cdlemk53b  30424  cdlemk53  30425  cdlemk55a  30427  cdlemk43N  30431  cdlemk19u1  30437  cdlemm10N  30587  cdlemn2  30664  cdlemn10  30675  dihjustlem  30685  dihord2cN  30690  dihvalcq2  30716  dihopelvalcpre  30717  dihord5b  30728  dihord6b  30729  dihmeetlem2N  30768  dihmeetbclemN  30773  dihmeetlem4preN  30775  dihmeetALTN  30796  dochshpncl  30853  dochsatshpb  30921  hdmapval3N  31310  hgmap11  31374
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