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  2962  funprg  5459  omeulem2  6785  uniinqs  6943  unxpdomlem3  7274  elfiun  7393  cofsmo  8105  isfin2-2  8155  isf32lem9  8197  tskun  8617  tskurn  8620  reclem3pr  8882  dmdcan  9680  lt2msq1  9849  supmullem1  9930  supmul  9932  xaddass2  10785  xlt2add  10795  xmulasslem3  10821  iccsplit  10985  expaddzlem  11378  expaddz  11379  expmulz  11381  limsupgle  12226  o1add  12362  o1mul  12363  o1sub  12364  bitsfzo  12902  sadfval  12919  smufval  12944  prmexpb  13072  4sqlem18  13285  vdwlem10  13313  mrieqv2d  13819  curf1  14277  spwpr4  14618  mndodcong  15135  subgabl  15410  gex2abl  15421  cntzsubr  15855  abvres  15882  lbsind2  16108  lbsextlem2  16186  lbsextg  16189  cnprest  17307  isreg2  17395  fbssfi  17822  hausflimlem  17964  tmdgsum  18078  ssblps  18405  ssbl  18406  xrsmopn  18796  dvres2  19752  vieta1  20182  aalioulem4  20205  cxpadd  20523  cxpsub  20526  divcxp  20531  cxple2  20541  cxplt2  20542  cxpcn3lem  20584  angcan  20597  ang180lem5  20608  isosctrlem3  20617  chscllem4  23095  pstmval  24243  measinblem  24527  cvmlift2lem6  24948  dedekind  25140  poseq  25467  brbtwn2  25748  axcontlem4  25810  axcontlem8  25814  linethru  25991  cnres2  26362  pellfundex  26839  congtr  26920  fzmaxdif  26936  isnumbasgrplem2  27137  matrng  27348  idomsubgmo  27382  stoweidlem31  27647  lcv1  29524  lfl1  29553  lshpkrex  29601  hlrelat3  29894  cvrval3  29895  cvrval4N  29896  athgt  29938  atcvrlln2  30001  atcvrlln  30002  lvolnle3at  30064  lvolnlelpln  30067  4atlem11  30091  4atlem12  30094  2lplnj  30102  dalemddea  30166  cdlema2N  30274  paddasslem2  30303  atmod1i1m  30340  lhp2lt  30483  lhp0lt  30485  lhpexle3lem  30493  lhpj1  30504  lhpmcvr4N  30508  lhpelim  30519  lhpmod2i2  30520  lhpmod6i1  30521  cdlemb2  30523  lhpat  30525  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrncnv  30628  ltrnmw  30633  trlval2  30645  trljat1  30648  trljat2  30649  trlnidatb  30659  cdlemc1  30673  cdlemc2  30674  cdlemc5  30677  cdlemc6  30678  cdleme0aa  30692  cdleme0b  30694  cdleme0c  30695  cdleme0e  30699  cdleme0fN  30700  cdleme01N  30703  cdleme0ex1N  30705  cdleme0moN  30707  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme4a  30721  cdleme5  30722  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme16aN  30741  cdleme11fN  30746  cdleme11g  30747  cdleme11k  30750  cdleme13  30754  cdleme17c  30770  cdleme17d1  30771  cdleme18c  30775  cdleme22gb  30776  cdlemeda  30780  cdlemednpq  30781  cdlemednuN  30782  cdleme19c  30787  cdleme20aN  30791  cdleme20bN  30792  cdleme20c  30793  cdleme22aa  30821  cdleme22d  30825  cdleme22e  30826  cdleme27cl  30848  cdleme27a  30849  cdleme30a  30860  cdleme42a  30953  cdleme42c  30954  cdlemg2fv2  31082  cdlemg2m  31086  cdlemg4g  31098  cdlemg4  31099  cdlemg6c  31102  cdlemg7aN  31107  cdlemg9a  31114  cdlemg9b  31115  cdlemg10c  31121  cdlemg12a  31125  cdlemg12b  31126  cdlemg17a  31143  cdlemg18b  31161  cdlemg18c  31162  trlcoabs2N  31204  trlcolem  31208  tendoco2  31250  tendoicl  31278  cdlemi1  31300  cdlemi2  31301  cdlemj3  31305  tendocan  31306  cdlemk3  31315  cdlemk4  31316  cdlemk5a  31317  cdlemk9  31321  cdlemk9bN  31322  cdlemk10  31325  cdlemk30  31376  cdlemk31  31378  cdlemk39  31398  cdlemkfid1N  31403  cdlemkfid2N  31405  cdlemk19ylem  31412  cdlemk19xlem  31424  cdlemk53b  31438  cdlemk53  31439  cdlemk55a  31441  cdlemk43N  31445  cdlemk19u1  31451  cdlemm10N  31601  cdlemn2  31678  cdlemn10  31689  dihjustlem  31699  dihord2cN  31704  dihvalcq2  31730  dihopelvalcpre  31731  dihord5b  31742  dihord6b  31743  dihmeetlem2N  31782  dihmeetbclemN  31787  dihmeetlem4preN  31789  dihmeetALTN  31810  dochshpncl  31867  dochsatshpb  31935  hdmapval3N  32324  hgmap11  32388
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