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

Theorem simp2r 1021
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2r  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 459 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 1016 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simpl2r  1048  simpr2r  1054  simp12r  1108  simp22r  1114  simp32r  1120  funprg  5545  fsnunf  6011  f1oiso2  6149  fnsuppres  6845  omeulem2  7150  uniinqs  7309  unxpdomlem3  7642  fin23lem11  8610  reclem3pr  9338  dedekind  9655  addid2  9674  dmdcan  10171  xaddass2  11363  xlt2add  11373  xadddi2  11410  expaddzlem  12112  expaddz  12113  expmulz  12115  expdiv  12119  ccatopth2  12607  relexpaddnn  12886  o1add  13438  o1mul  13439  o1sub  13440  ntrivcvgmul  13713  prmexpb  14260  pcpremul  14369  pcdiv  14378  pcqmul  14379  pcqdiv  14383  4sqlem12  14476  f1ocpbllem  14931  ercpbl  14956  erlecpbl  14957  latjlej12  15814  latmlem12  15830  latj4  15848  symgsssg  16609  symgfisg  16610  mndodcong  16683  cmn4  16934  ablsub4  16940  abladdsub4  16941  lsm4  16983  abvdom  17600  abvtrivd  17602  lspsnvs  17873  lspsneu  17882  lspfixed  17887  lspexch  17888  lsmcv  17900  lspsolvlem  17901  mvrf1  18194  coe1sclmulfv  18437  m1detdiag  19184  cnprest  19876  isreg2  19964  elptr  20159  hausflimlem  20565  trcfilu  20882  ssblps  21010  ssbl  21011  prdsxmslem2  21117  tgqioo  21390  metnrm  21451  bndth  21543  cph2ass  21744  iscau3  21802  ovolunlem2  21994  dvres2  22401  dvfsumlem2  22513  dvfsum2  22520  deg1tm  22604  plyadd  22699  plymul  22700  coeeu  22707  coemullem  22732  aalioulem4  22816  cxplea  23164  cxple2  23165  cxplt2  23166  cxple2a  23167  cxpcn3lem  23208  angcan  23252  ang180lem5  23263  divsqrtsumlem  23426  logexprlim  23617  dchrvmasumlema  23802  dchrisum0lema  23816  logdivsum  23835  log2sumbnd  23846  padicabv  23932  tghilberti2  24138  brbtwn2  24329  axcontlem4  24391  axcontlem8  24395  1pthon  24714  chscllem4  26675  mdslmd4i  27368  orngmul  27947  nexple  28158  measxun2  28337  measun  28338  mbfmco2  28392  probun  28541  wsuclem  29546  cgrcomim  29792  cgrcoml  29799  cgrcomr  29800  cgrdegen  29807  btwnintr  29822  btwnexch3  29823  btwnouttr  29827  btwnexch  29828  btwndiff  29830  ifscgr  29847  lineid  29886  btwnconn1lem7  29896  btwnconn1lem8  29897  btwnconn1lem9  29898  btwnconn1lem12  29901  midofsegid  29907  brsegle2  29912  btwnoutside  29928  outsideoftr  29932  cnres2  30425  heibor  30483  mzpmfp  30845  mzpsubst  30846  pellexlem5  30934  pell14qrexpclnn0  30967  pellfundex  30987  qirropth  31009  monotuz  31042  expmordi  31048  congmul  31070  congsub  31073  mzpcong  31075  fzmaxdif  31084  jm2.15nn0  31111  idomsubgmo  31323  fourierdlem42  32097  fourierdlem48  32103  fourierdlem80  32135  lidldomn1  32927  rngccatidALTV  32997  ringccatidALTV  33060  coe1sclmulval  33185  lsmsat  35146  lkrlsp  35240  lkrlsp2  35241  lkrlsp3  35242  lshpkrlem6  35253  latm4  35371  omlspjN  35399  hlatj4  35511  4noncolr3  35590  4noncolr2  35591  4noncolr1  35592  3dimlem3a  35597  3dimlem4a  35600  3dimlem4  35601  3dimlem4OLDN  35602  1cvratex  35610  hlatexch4  35618  3atlem4  35623  atcvrlln2  35656  atcvrlln  35657  llnmlplnN  35676  lplnnlelln  35680  lvoli2  35718  lvolnlelln  35721  lvolnlelpln  35722  4atlem11b  35745  4atlem12b  35748  2lplnj  35757  dalemzeo  35770  dath2  35874  lncvrat  35919  cdlemb  35931  elpaddri  35939  padd4N  35977  llnmod2i2  36000  llnexchb2  36006  dalawlem1  36008  dalawlem2  36009  osumcllem6N  36098  pexmidlem3N  36109  pexmidlem4N  36110  lhp2lt  36138  lhp2at0  36169  lhp2atne  36171  lhp2at0ne  36173  lhpmod2i2  36175  lhpmod6i1  36176  lhpat  36180  lhpat3  36183  4atexlemex6  36211  ltrncoval  36282  ltrncnv  36283  ltrnnidn  36312  cdlemd7  36342  cdleme0b  36350  cdleme0c  36351  cdleme0fN  36356  cdleme0ex1N  36361  cdleme7d  36384  cdleme7e  36385  cdleme7ga  36386  cdleme7  36387  cdleme11a  36398  cdleme17c  36426  cdleme22gb  36432  cdlemeda  36436  cdleme20k  36458  cdleme21a  36464  cdleme21at  36467  cdleme21d  36469  cdleme22f2  36486  cdleme22g  36487  cdleme24  36491  cdleme28  36512  cdlemefrs29cpre1  36537  cdlemefr29exN  36541  cdlemefr32sn2aw  36543  cdleme32fva  36576  cdleme32fva1  36577  cdleme35a  36587  cdleme42c  36611  cdleme42e  36618  cdleme42f  36619  cdleme42g  36620  cdleme42h  36621  cdleme43bN  36629  cdleme46f2g2  36632  cdleme17d2  36634  cdleme4gfv  36646  cdlemeg46c  36652  cdlemeg46nlpq  36656  cdlemeg46gfre  36671  cdlemeg49lebilem  36678  cdleme50trn1  36688  cdleme50trn2  36690  cdleme50ltrn  36696  cdleme  36699  cdlemf1  36700  cdlemf  36702  trlord  36708  ltrniotavalbN  36723  cdlemg1cex  36727  cdlemg2dN  36729  cdlemg2ce  36731  cdlemg2fvlem  36733  cdlemg2idN  36735  cdlemg2kq  36741  cdlemg2l  36742  cdlemg7fvN  36763  cdlemg7aN  36764  cdlemg8a  36766  cdlemg11aq  36777  cdlemg12d  36785  cdlemg13a  36790  cdlemg13  36791  cdlemg14f  36792  cdlemg14g  36793  cdlemg17b  36801  cdlemg27a  36831  cdlemg31b0N  36833  cdlemg31a  36836  cdlemg31b  36837  cdlemg31c  36838  ltrnco  36858  trlcoabs2N  36861  trlcocnvat  36863  trlconid  36864  trlcolem  36865  cdlemg42  36868  cdlemg43  36869  cdlemg47a  36873  cdlemg46  36874  cdlemg47  36875  tendoeq1  36903  tendocoval  36905  tendoco2  36907  tendoplco2  36918  tendopltp  36919  cdlemh1  36954  cdlemh2  36955  cdlemi1  36957  cdlemi  36959  cdlemk1  36970  cdlemk2  36971  cdlemk3  36972  cdlemk4  36973  cdlemk8  36977  cdlemk9  36978  cdlemk9bN  36979  cdlemk31  37035  cdlemk28-3  37047  cdlemk19xlem  37081  cdlemk39u  37107  cdlemk19u  37109  cdlemk56w  37112  cdlemn7  37343  cdlemn8  37344  cdlemn9  37345  dihordlem6  37353  dihordlem7  37354  dihordlem7b  37355  dihord1  37358  dihord2a  37359  dihord11c  37364  dihord2pre  37365  dihord2pre2  37366  dihlsscpre  37374  dihord4  37398  dihord6b  37400  dihmeetlem2N  37439  dihglbcpreN  37440  dihmeetcN  37442  dihmeetbclemN  37444  dihmeetlem3N  37445  dihmeetlem9N  37455  dihmeetlem13N  37459  dihmeetlem20N  37466  mapdpglem24  37844  mapdpglem32  37845  baerlem3lem2  37850  baerlem5alem2  37851  baerlem5blem2  37852  mapdh9aOLDN  37931  hdmap14lem6  38016  trclimalb2  38257
  Copyright terms: Public domain W3C validator