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

Theorem simp1r 1008
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 458 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1004 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  simpl1r  1035  simpr1r  1041  simp11r  1095  simp21r  1101  simp31r  1107  vtoclgft  3017  funprg  5464  omeulem2  7018  uniinqs  7176  unxpdomlem3  7515  elfiun  7676  cofsmo  8434  isfin2-2  8484  isf32lem9  8526  tskun  8949  tskurn  8952  reclem3pr  9214  dedekind  9529  dmdcan  10037  lt2msq1  10211  supmullem1  10292  supmul  10294  xaddass2  11209  xlt2add  11219  xmulasslem3  11245  iccsplit  11414  expaddzlem  11903  expaddz  11904  expmulz  11906  limsupgle  12951  o1add  13087  o1mul  13088  o1sub  13089  bitsfzo  13627  sadfval  13644  smufval  13669  prmexpb  13799  4sqlem18  14019  vdwlem10  14047  mrieqv2d  14573  curf1  15031  mndodcong  16038  subgabl  16313  gex2abl  16326  cntzsubr  16877  abvres  16904  lbsind2  17140  lbsextlem2  17218  lbsextg  17221  matrng  18230  mdetunilem8  18325  maducoeval  18345  maducoeval2  18346  madurid  18350  cramerimplem3  18391  cnprest  18793  isreg2  18881  fbssfi  19310  hausflimlem  19452  tmdgsum  19566  ssblps  19897  ssbl  19898  xrsmopn  20289  dvres2  21287  vieta1  21721  aalioulem4  21744  cxpadd  22067  cxpsub  22070  divcxp  22075  cxple2  22085  cxplt2  22086  cxpcn3lem  22128  angcan  22141  ang180lem5  22152  isosctrlem3  22161  brbtwn2  23070  axcontlem4  23132  axcontlem8  23136  chscllem4  24962  ogrpinvlt  26104  pstmval  26242  measinblem  26554  cvmlift2lem6  27111  poseq  27627  linethru  28097  cnres2  28571  pellfundex  29136  congtr  29217  fzmaxdif  29233  isnumbasgrplem2  29369  idomsubgmo  29472  stoweidlem31  29735  clwwlknimp  30348  domnmsuppn0  30682  mndpfsupp  30689  lincext3  30814  lcv1  32374  lfl1  32403  lshpkrex  32451  hlrelat3  32744  cvrval3  32745  cvrval4N  32746  athgt  32788  atcvrlln2  32851  atcvrlln  32852  lvolnle3at  32914  lvolnlelpln  32917  4atlem11  32941  4atlem12  32944  2lplnj  32952  dalemddea  33016  cdlema2N  33124  paddasslem2  33153  atmod1i1m  33190  lhp2lt  33333  lhp0lt  33335  lhpexle3lem  33343  lhpj1  33354  lhpmcvr4N  33358  lhpelim  33369  lhpmod2i2  33370  lhpmod6i1  33371  cdlemb2  33373  lhpat  33375  ltrnatb  33469  ltrnel  33471  ltrncnvel  33474  ltrncnv  33478  ltrnmw  33483  trlval2  33495  trljat1  33498  trljat2  33499  trlnidatb  33509  cdlemc1  33523  cdlemc2  33524  cdlemc5  33527  cdlemc6  33528  cdleme0aa  33542  cdleme0b  33544  cdleme0c  33545  cdleme0e  33549  cdleme0fN  33550  cdleme01N  33553  cdleme0ex1N  33555  cdleme0moN  33557  cdleme3g  33566  cdleme3h  33567  cdleme3  33569  cdleme4  33570  cdleme4a  33571  cdleme5  33572  cdleme8  33582  cdleme9  33585  cdleme10  33586  cdleme16aN  33591  cdleme11fN  33596  cdleme11g  33597  cdleme11k  33600  cdleme13  33604  cdleme17c  33620  cdleme17d1  33621  cdleme18c  33625  cdleme22gb  33626  cdlemeda  33630  cdlemednpq  33631  cdlemednuN  33632  cdleme19c  33637  cdleme20aN  33641  cdleme20bN  33642  cdleme20c  33643  cdleme22aa  33671  cdleme22d  33675  cdleme22e  33676  cdleme27cl  33698  cdleme27a  33699  cdleme30a  33710  cdleme42a  33803  cdleme42c  33804  cdlemg2fv2  33932  cdlemg2m  33936  cdlemg4g  33948  cdlemg4  33949  cdlemg6c  33952  cdlemg7aN  33957  cdlemg9a  33964  cdlemg9b  33965  cdlemg10c  33971  cdlemg12a  33975  cdlemg12b  33976  cdlemg17a  33993  cdlemg18b  34011  cdlemg18c  34012  trlcoabs2N  34054  trlcolem  34058  tendoco2  34100  tendoicl  34128  cdlemi1  34150  cdlemi2  34151  cdlemj3  34155  tendocan  34156  cdlemk3  34165  cdlemk4  34166  cdlemk5a  34167  cdlemk9  34171  cdlemk9bN  34172  cdlemk10  34175  cdlemk30  34226  cdlemk31  34228  cdlemk39  34248  cdlemkfid1N  34253  cdlemkfid2N  34255  cdlemk19ylem  34262  cdlemk19xlem  34274  cdlemk53b  34288  cdlemk53  34289  cdlemk55a  34291  cdlemk43N  34295  cdlemk19u1  34301  cdlemm10N  34451  cdlemn2  34528  cdlemn10  34539  dihjustlem  34549  dihord2cN  34554  dihvalcq2  34580  dihopelvalcpre  34581  dihord5b  34592  dihord6b  34593  dihmeetlem2N  34632  dihmeetbclemN  34637  dihmeetlem4preN  34639  dihmeetALTN  34660  dochshpncl  34717  dochsatshpb  34785  hdmapval3N  35174  hgmap11  35238
  Copyright terms: Public domain W3C validator