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

Theorem simp1r 982
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 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl1r  1009  simpr1r  1015  simp11r  1069  simp21r  1075  simp31r  1081  vtoclgft  2966  funprg  5463  omeulem2  6789  uniinqs  6947  unxpdomlem3  7278  elfiun  7397  cofsmo  8109  isfin2-2  8159  isf32lem9  8201  tskun  8621  tskurn  8624  reclem3pr  8886  dmdcan  9684  lt2msq1  9853  supmullem1  9934  supmul  9936  xaddass2  10789  xlt2add  10799  xmulasslem3  10825  iccsplit  10989  expaddzlem  11382  expaddz  11383  expmulz  11385  limsupgle  12230  o1add  12366  o1mul  12367  o1sub  12368  bitsfzo  12906  sadfval  12923  smufval  12948  prmexpb  13076  4sqlem18  13289  vdwlem10  13317  mrieqv2d  13823  curf1  14281  spwpr4  14622  mndodcong  15139  subgabl  15414  gex2abl  15425  cntzsubr  15859  abvres  15886  lbsind2  16112  lbsextlem2  16190  lbsextg  16193  cnprest  17311  isreg2  17399  fbssfi  17826  hausflimlem  17968  tmdgsum  18082  ssblps  18409  ssbl  18410  xrsmopn  18800  dvres2  19756  vieta1  20186  aalioulem4  20209  cxpadd  20527  cxpsub  20530  divcxp  20535  cxple2  20545  cxplt2  20546  cxpcn3lem  20588  angcan  20601  ang180lem5  20612  isosctrlem3  20621  chscllem4  23099  pstmval  24247  measinblem  24531  cvmlift2lem6  24952  dedekind  25144  poseq  25471  brbtwn2  25752  axcontlem4  25814  axcontlem8  25818  linethru  25995  cnres2  26366  pellfundex  26843  congtr  26924  fzmaxdif  26940  isnumbasgrplem2  27141  matrng  27352  idomsubgmo  27386  stoweidlem31  27651  lcv1  29528  lfl1  29557  lshpkrex  29605  hlrelat3  29898  cvrval3  29899  cvrval4N  29900  athgt  29942  atcvrlln2  30005  atcvrlln  30006  lvolnle3at  30068  lvolnlelpln  30071  4atlem11  30095  4atlem12  30098  2lplnj  30106  dalemddea  30170  cdlema2N  30278  paddasslem2  30307  atmod1i1m  30344  lhp2lt  30487  lhp0lt  30489  lhpexle3lem  30497  lhpj1  30508  lhpmcvr4N  30512  lhpelim  30523  lhpmod2i2  30524  lhpmod6i1  30525  cdlemb2  30527  lhpat  30529  ltrnatb  30623  ltrnel  30625  ltrncnvel  30628  ltrncnv  30632  ltrnmw  30637  trlval2  30649  trljat1  30652  trljat2  30653  trlnidatb  30663  cdlemc1  30677  cdlemc2  30678  cdlemc5  30681  cdlemc6  30682  cdleme0aa  30696  cdleme0b  30698  cdleme0c  30699  cdleme0e  30703  cdleme0fN  30704  cdleme01N  30707  cdleme0ex1N  30709  cdleme0moN  30711  cdleme3g  30720  cdleme3h  30721  cdleme3  30723  cdleme4  30724  cdleme4a  30725  cdleme5  30726  cdleme8  30736  cdleme9  30739  cdleme10  30740  cdleme16aN  30745  cdleme11fN  30750  cdleme11g  30751  cdleme11k  30754  cdleme13  30758  cdleme17c  30774  cdleme17d1  30775  cdleme18c  30779  cdleme22gb  30780  cdlemeda  30784  cdlemednpq  30785  cdlemednuN  30786  cdleme19c  30791  cdleme20aN  30795  cdleme20bN  30796  cdleme20c  30797  cdleme22aa  30825  cdleme22d  30829  cdleme22e  30830  cdleme27cl  30852  cdleme27a  30853  cdleme30a  30864  cdleme42a  30957  cdleme42c  30958  cdlemg2fv2  31086  cdlemg2m  31090  cdlemg4g  31102  cdlemg4  31103  cdlemg6c  31106  cdlemg7aN  31111  cdlemg9a  31118  cdlemg9b  31119  cdlemg10c  31125  cdlemg12a  31129  cdlemg12b  31130  cdlemg17a  31147  cdlemg18b  31165  cdlemg18c  31166  trlcoabs2N  31208  trlcolem  31212  tendoco2  31254  tendoicl  31282  cdlemi1  31304  cdlemi2  31305  cdlemj3  31309  tendocan  31310  cdlemk3  31319  cdlemk4  31320  cdlemk5a  31321  cdlemk9  31325  cdlemk9bN  31326  cdlemk10  31329  cdlemk30  31380  cdlemk31  31382  cdlemk39  31402  cdlemkfid1N  31407  cdlemkfid2N  31409  cdlemk19ylem  31416  cdlemk19xlem  31428  cdlemk53b  31442  cdlemk53  31443  cdlemk55a  31445  cdlemk43N  31449  cdlemk19u1  31455  cdlemm10N  31605  cdlemn2  31682  cdlemn10  31693  dihjustlem  31703  dihord2cN  31708  dihvalcq2  31734  dihopelvalcpre  31735  dihord5b  31746  dihord6b  31747  dihmeetlem2N  31786  dihmeetbclemN  31791  dihmeetlem4preN  31793  dihmeetALTN  31814  dochshpncl  31871  dochsatshpb  31939  hdmapval3N  32328  hgmap11  32392
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator