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

Theorem simp1r 981
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 977 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  simpl1r  1008  simpr1r  1014  simp11r  1068  simp21r  1074  simp31r  1080  vtoclgft  2919  funprg  5404  omeulem2  6723  uniinqs  6881  unxpdomlem3  7212  elfiun  7330  cofsmo  8042  isfin2-2  8092  isf32lem9  8134  tskun  8555  tskurn  8558  reclem3pr  8820  dmdcan  9617  lt2msq1  9786  supmullem1  9867  supmul  9869  xaddass2  10722  xlt2add  10732  xmulasslem3  10758  iccsplit  10921  expaddzlem  11310  expaddz  11311  expmulz  11313  limsupgle  12158  o1add  12294  o1mul  12295  o1sub  12296  bitsfzo  12834  sadfval  12851  smufval  12876  prmexpb  13004  4sqlem18  13217  vdwlem10  13245  mrieqv2d  13751  curf1  14209  spwpr4  14550  mndodcong  15067  subgabl  15342  gex2abl  15353  cntzsubr  15787  abvres  15814  lbsind2  16044  lbsextlem2  16122  lbsextg  16125  cnprest  17234  isreg2  17322  fbssfi  17745  hausflimlem  17887  tmdgsum  17991  ssbl  18184  xrsmopn  18531  dvres2  19477  vieta1  19907  aalioulem4  19930  cxpadd  20248  cxpsub  20251  divcxp  20256  cxple2  20266  cxplt2  20267  cxpcn3lem  20309  angcan  20322  ang180lem5  20333  isosctrlem3  20342  chscllem4  22653  measinblem  24158  cvmlift2lem6  24563  dedekind  24756  poseq  25079  brbtwn2  25360  axcontlem4  25422  axcontlem8  25426  linethru  25603  cnres2  26074  pellfundex  26562  congtr  26643  fzmaxdif  26659  isnumbasgrplem2  26860  matrng  27071  idomsubgmo  27105  stoweidlem31  27371  lcv1  29290  lfl1  29319  lshpkrex  29367  hlrelat3  29660  cvrval3  29661  cvrval4N  29662  athgt  29704  atcvrlln2  29767  atcvrlln  29768  lvolnle3at  29830  lvolnlelpln  29833  4atlem11  29857  4atlem12  29860  2lplnj  29868  dalemddea  29932  cdlema2N  30040  paddasslem2  30069  atmod1i1m  30106  lhp2lt  30249  lhp0lt  30251  lhpexle3lem  30259  lhpj1  30270  lhpmcvr4N  30274  lhpelim  30285  lhpmod2i2  30286  lhpmod6i1  30287  cdlemb2  30289  lhpat  30291  ltrnatb  30385  ltrnel  30387  ltrncnvel  30390  ltrncnv  30394  ltrnmw  30399  trlval2  30411  trljat1  30414  trljat2  30415  trlnidatb  30425  cdlemc1  30439  cdlemc2  30440  cdlemc5  30443  cdlemc6  30444  cdleme0aa  30458  cdleme0b  30460  cdleme0c  30461  cdleme0e  30465  cdleme0fN  30466  cdleme01N  30469  cdleme0ex1N  30471  cdleme0moN  30473  cdleme3g  30482  cdleme3h  30483  cdleme3  30485  cdleme4  30486  cdleme4a  30487  cdleme5  30488  cdleme8  30498  cdleme9  30501  cdleme10  30502  cdleme16aN  30507  cdleme11fN  30512  cdleme11g  30513  cdleme11k  30516  cdleme13  30520  cdleme17c  30536  cdleme17d1  30537  cdleme18c  30541  cdleme22gb  30542  cdlemeda  30546  cdlemednpq  30547  cdlemednuN  30548  cdleme19c  30553  cdleme20aN  30557  cdleme20bN  30558  cdleme20c  30559  cdleme22aa  30587  cdleme22d  30591  cdleme22e  30592  cdleme27cl  30614  cdleme27a  30615  cdleme30a  30626  cdleme42a  30719  cdleme42c  30720  cdlemg2fv2  30848  cdlemg2m  30852  cdlemg4g  30864  cdlemg4  30865  cdlemg6c  30868  cdlemg7aN  30873  cdlemg9a  30880  cdlemg9b  30881  cdlemg10c  30887  cdlemg12a  30891  cdlemg12b  30892  cdlemg17a  30909  cdlemg18b  30927  cdlemg18c  30928  trlcoabs2N  30970  trlcolem  30974  tendoco2  31016  tendoicl  31044  cdlemi1  31066  cdlemi2  31067  cdlemj3  31071  tendocan  31072  cdlemk3  31081  cdlemk4  31082  cdlemk5a  31083  cdlemk9  31087  cdlemk9bN  31088  cdlemk10  31091  cdlemk30  31142  cdlemk31  31144  cdlemk39  31164  cdlemkfid1N  31169  cdlemkfid2N  31171  cdlemk19ylem  31178  cdlemk19xlem  31190  cdlemk53b  31204  cdlemk53  31205  cdlemk55a  31207  cdlemk43N  31211  cdlemk19u1  31217  cdlemm10N  31367  cdlemn2  31444  cdlemn10  31455  dihjustlem  31465  dihord2cN  31470  dihvalcq2  31496  dihopelvalcpre  31497  dihord5b  31508  dihord6b  31509  dihmeetlem2N  31548  dihmeetbclemN  31553  dihmeetlem4preN  31555  dihmeetALTN  31576  dochshpncl  31633  dochsatshpb  31701  hdmapval3N  32090  hgmap11  32154
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 937
  Copyright terms: Public domain W3C validator