MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1r Structured version   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  3002  funprg  5500  omeulem2  6826  uniinqs  6984  unxpdomlem3  7315  elfiun  7435  cofsmo  8149  isfin2-2  8199  isf32lem9  8241  tskun  8661  tskurn  8664  reclem3pr  8926  dmdcan  9724  lt2msq1  9893  supmullem1  9974  supmul  9976  xaddass2  10829  xlt2add  10839  xmulasslem3  10865  iccsplit  11029  expaddzlem  11423  expaddz  11424  expmulz  11426  limsupgle  12271  o1add  12407  o1mul  12408  o1sub  12409  bitsfzo  12947  sadfval  12964  smufval  12989  prmexpb  13117  4sqlem18  13330  vdwlem10  13358  mrieqv2d  13864  curf1  14322  spwpr4  14663  mndodcong  15180  subgabl  15455  gex2abl  15466  cntzsubr  15900  abvres  15927  lbsind2  16153  lbsextlem2  16231  lbsextg  16234  cnprest  17353  isreg2  17441  fbssfi  17869  hausflimlem  18011  tmdgsum  18125  ssblps  18452  ssbl  18453  xrsmopn  18843  dvres2  19799  vieta1  20229  aalioulem4  20252  cxpadd  20570  cxpsub  20573  divcxp  20578  cxple2  20588  cxplt2  20589  cxpcn3lem  20631  angcan  20644  ang180lem5  20655  isosctrlem3  20664  chscllem4  23142  pstmval  24290  measinblem  24574  cvmlift2lem6  24995  dedekind  25187  poseq  25528  brbtwn2  25844  axcontlem4  25906  axcontlem8  25910  linethru  26087  cnres2  26472  pellfundex  26949  congtr  27030  fzmaxdif  27046  isnumbasgrplem2  27246  matrng  27457  idomsubgmo  27491  stoweidlem31  27756  lcv1  29839  lfl1  29868  lshpkrex  29916  hlrelat3  30209  cvrval3  30210  cvrval4N  30211  athgt  30253  atcvrlln2  30316  atcvrlln  30317  lvolnle3at  30379  lvolnlelpln  30382  4atlem11  30406  4atlem12  30409  2lplnj  30417  dalemddea  30481  cdlema2N  30589  paddasslem2  30618  atmod1i1m  30655  lhp2lt  30798  lhp0lt  30800  lhpexle3lem  30808  lhpj1  30819  lhpmcvr4N  30823  lhpelim  30834  lhpmod2i2  30835  lhpmod6i1  30836  cdlemb2  30838  lhpat  30840  ltrnatb  30934  ltrnel  30936  ltrncnvel  30939  ltrncnv  30943  ltrnmw  30948  trlval2  30960  trljat1  30963  trljat2  30964  trlnidatb  30974  cdlemc1  30988  cdlemc2  30989  cdlemc5  30992  cdlemc6  30993  cdleme0aa  31007  cdleme0b  31009  cdleme0c  31010  cdleme0e  31014  cdleme0fN  31015  cdleme01N  31018  cdleme0ex1N  31020  cdleme0moN  31022  cdleme3g  31031  cdleme3h  31032  cdleme3  31034  cdleme4  31035  cdleme4a  31036  cdleme5  31037  cdleme8  31047  cdleme9  31050  cdleme10  31051  cdleme16aN  31056  cdleme11fN  31061  cdleme11g  31062  cdleme11k  31065  cdleme13  31069  cdleme17c  31085  cdleme17d1  31086  cdleme18c  31090  cdleme22gb  31091  cdlemeda  31095  cdlemednpq  31096  cdlemednuN  31097  cdleme19c  31102  cdleme20aN  31106  cdleme20bN  31107  cdleme20c  31108  cdleme22aa  31136  cdleme22d  31140  cdleme22e  31141  cdleme27cl  31163  cdleme27a  31164  cdleme30a  31175  cdleme42a  31268  cdleme42c  31269  cdlemg2fv2  31397  cdlemg2m  31401  cdlemg4g  31413  cdlemg4  31414  cdlemg6c  31417  cdlemg7aN  31422  cdlemg9a  31429  cdlemg9b  31430  cdlemg10c  31436  cdlemg12a  31440  cdlemg12b  31441  cdlemg17a  31458  cdlemg18b  31476  cdlemg18c  31477  trlcoabs2N  31519  trlcolem  31523  tendoco2  31565  tendoicl  31593  cdlemi1  31615  cdlemi2  31616  cdlemj3  31620  tendocan  31621  cdlemk3  31630  cdlemk4  31631  cdlemk5a  31632  cdlemk9  31636  cdlemk9bN  31637  cdlemk10  31640  cdlemk30  31691  cdlemk31  31693  cdlemk39  31713  cdlemkfid1N  31718  cdlemkfid2N  31720  cdlemk19ylem  31727  cdlemk19xlem  31739  cdlemk53b  31753  cdlemk53  31754  cdlemk55a  31756  cdlemk43N  31760  cdlemk19u1  31766  cdlemm10N  31916  cdlemn2  31993  cdlemn10  32004  dihjustlem  32014  dihord2cN  32019  dihvalcq2  32045  dihopelvalcpre  32046  dihord5b  32057  dihord6b  32058  dihmeetlem2N  32097  dihmeetbclemN  32102  dihmeetlem4preN  32104  dihmeetALTN  32125  dochshpncl  32182  dochsatshpb  32250  hdmapval3N  32639  hgmap11  32703
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