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

Theorem simp1r 1030
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 462 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1026 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl1r  1057  simpr1r  1063  simp11r  1117  simp21r  1123  simp31r  1129  vtoclgft  3135  funprg  5650  omeulem2  7292  uniinqs  7451  unxpdomlem3  7784  elfiun  7950  cofsmo  8697  isfin2-2  8747  isf32lem9  8789  tskun  9210  tskurn  9213  reclem3pr  9473  dedekind  9796  dmdcan  10316  lt2msq1  10489  supmullem1  10577  supmul  10579  xaddass2  11536  xlt2add  11546  xmulasslem3  11572  iccsplit  11763  expaddzlem  12312  expaddz  12313  expmulz  12315  limsupgle  13513  o1add  13655  o1mul  13656  o1sub  13657  bitsfzo  14383  sadfval  14400  smufval  14425  prmexpb  14641  4sqlem18OLD  14869  4sqlem18  14875  vdwlem10  14903  mrieqv2d  15496  curf1  16061  mndodcong  17133  subgabl  17411  gex2abl  17424  cntzsubr  17975  abvres  18002  lbsind2  18239  lbsextlem2  18317  lbsextg  18320  matring  19399  mdetunilem8  19575  maducoeval  19595  maducoeval2  19596  madurid  19600  cramerimplem3  19641  pmatcollpw2  19733  pm2mpf1  19754  cnprest  20236  isreg2  20324  fbssfi  20783  hausflimlem  20925  tmdgsum  21041  ssblps  21368  ssbl  21369  xrsmopn  21741  dvres2  22744  vieta1  23133  aalioulem4  23156  efgh  23355  cxpadd  23489  cxpsub  23492  divcxp  23497  cxple2  23507  cxplt2  23508  cxpcn3lem  23552  angcan  23596  ang180lem5  23607  isosctrlem3  23614  brbtwn2  24781  axcontlem4  24843  axcontlem8  24847  clwwlknimp  25349  chscllem4  27128  ogrpinvlt  28325  pstmval  28537  measinblem  28881  cvmlift2lem6  29819  poseq  30278  linethru  30705  cnres2  31799  lcv1  32316  lfl1  32345  lshpkrex  32393  hlrelat3  32686  cvrval3  32687  cvrval4N  32688  athgt  32730  atcvrlln2  32793  atcvrlln  32794  lvolnle3at  32856  lvolnlelpln  32859  4atlem11  32883  4atlem12  32886  2lplnj  32894  dalemddea  32958  cdlema2N  33066  paddasslem2  33095  atmod1i1m  33132  lhp2lt  33275  lhp0lt  33277  lhpexle3lem  33285  lhpj1  33296  lhpmcvr4N  33300  lhpelim  33311  lhpmod2i2  33312  lhpmod6i1  33313  cdlemb2  33315  lhpat  33317  ltrnatb  33411  ltrnel  33413  ltrncnvel  33416  ltrncnv  33420  ltrnmwOLD  33426  trlval2  33438  trljat1  33441  trljat2  33442  trlnidatb  33452  cdlemc1  33466  cdlemc2  33467  cdlemc5  33470  cdlemc6  33471  cdleme0aa  33485  cdleme0b  33487  cdleme0c  33488  cdleme0e  33492  cdleme0fN  33493  cdleme01N  33496  cdleme0ex1N  33498  cdleme0moN  33500  cdleme3g  33509  cdleme3h  33510  cdleme3  33512  cdleme4  33513  cdleme4a  33514  cdleme5  33515  cdleme8  33525  cdleme9  33528  cdleme10  33529  cdleme16aN  33534  cdleme11fN  33539  cdleme11g  33540  cdleme11k  33543  cdleme13  33547  cdleme17c  33563  cdleme17d1  33564  cdleme18c  33568  cdleme22gb  33569  cdlemeda  33573  cdlemednpq  33574  cdlemednuN  33575  cdleme19c  33581  cdleme20aN  33585  cdleme20bN  33586  cdleme20c  33587  cdleme22aa  33615  cdleme22d  33619  cdleme22e  33620  cdleme27cl  33642  cdleme27a  33643  cdleme30a  33654  cdleme42a  33747  cdleme42c  33748  cdlemg2fv2  33876  cdlemg2m  33880  cdlemg4g  33892  cdlemg4  33893  cdlemg6c  33896  cdlemg7aN  33901  cdlemg9a  33908  cdlemg9b  33909  cdlemg10c  33915  cdlemg12a  33919  cdlemg12b  33920  cdlemg17a  33937  cdlemg18b  33955  cdlemg18c  33956  trlcoabs2N  33998  trlcolem  34002  tendoco2  34044  tendoicl  34072  cdlemi1  34094  cdlemi2  34095  cdlemj3  34099  tendocan  34100  cdlemk3  34109  cdlemk4  34110  cdlemk5a  34111  cdlemk9  34115  cdlemk9bN  34116  cdlemk10  34119  cdlemk30  34170  cdlemk31  34172  cdlemk39  34192  cdlemkfid1N  34197  cdlemkfid2N  34199  cdlemk19ylem  34206  cdlemk19xlem  34218  cdlemk53b  34232  cdlemk53  34233  cdlemk55a  34235  cdlemk43N  34239  cdlemk19u1  34245  cdlemm10N  34395  cdlemn2  34472  cdlemn10  34483  dihjustlem  34493  dihord2cN  34498  dihvalcq2  34524  dihopelvalcpre  34525  dihord5b  34536  dihord6b  34537  dihmeetlem2N  34576  dihmeetbclemN  34581  dihmeetlem4preN  34583  dihmeetALTN  34604  dochshpncl  34661  dochsatshpb  34729  hdmapval3N  35118  hgmap11  35182  pellfundex  35440  congtr  35521  fzmaxdif  35537  isnumbasgrplem2  35669  idomsubgmo  35771  upbdrech  37132  suplesup  37171  mullimc  37268  islptre  37271  mullimcf  37275  neglimc  37300  icccncfext  37337  dvmptfprod  37389  stoweidlem31  37461  domnmsuppn0  38914  mndpfsupp  38921  lincext3  39009
  Copyright terms: Public domain W3C validator