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

Theorem simp2r 1023
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 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 1018 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  simpl2r  1050  simpr2r  1056  simp12r  1110  simp22r  1116  simp32r  1122  funprg  5643  fsnunf  6110  f1oiso2  6247  fnsuppres  6939  omeulem2  7244  uniinqs  7403  unxpdomlem3  7738  fin23lem11  8709  reclem3pr  9439  dedekind  9755  addid2  9774  dmdcan  10266  xaddass2  11454  xlt2add  11464  xadddi2  11501  expaddzlem  12189  expaddz  12190  expmulz  12192  expdiv  12196  ccatopth2  12675  o1add  13415  o1mul  13416  o1sub  13417  prmexpb  14133  pcpremul  14242  pcdiv  14251  pcqmul  14252  pcqdiv  14256  4sqlem12  14349  f1ocpbllem  14795  ercpbl  14820  erlecpbl  14821  latjlej12  15570  latmlem12  15586  latj4  15604  symgsssg  16363  symgfisg  16364  mndodcong  16437  cmn4  16688  ablsub4  16694  abladdsub4  16695  lsm4  16737  abvdom  17356  abvtrivd  17358  lspsnvs  17629  lspsneu  17638  lspfixed  17643  lspexch  17644  lsmcv  17656  lspsolvlem  17657  mvrf1  17949  coe1sclmulfv  18192  m1detdiag  18966  cnprest  19656  isreg2  19744  elptr  19940  hausflimlem  20346  trcfilu  20663  ssblps  20791  ssbl  20792  prdsxmslem2  20898  tgqioo  21171  metnrm  21232  bndth  21324  cph2ass  21525  iscau3  21583  ovolunlem2  21775  dvres2  22182  dvfsumlem2  22294  dvfsum2  22301  deg1tm  22385  plyadd  22480  plymul  22481  coeeu  22488  coemullem  22512  aalioulem4  22596  cxplea  22941  cxple2  22942  cxplt2  22943  cxple2a  22944  cxpcn3lem  22985  angcan  22998  ang180lem5  23009  divsqrtsumlem  23173  logexprlim  23364  dchrvmasumlema  23549  dchrisum0lema  23563  logdivsum  23582  log2sumbnd  23593  padicabv  23679  tghilbert1_2  23877  brbtwn2  24040  axcontlem4  24102  axcontlem8  24106  1pthon  24425  chscllem4  26389  mdslmd4i  27083  orngmul  27625  nexple  27837  measxun2  28013  measun  28014  mbfmco2  28068  probun  28190  ntrivcvgmul  28970  wsuclem  29315  cgrcomim  29573  cgrcoml  29580  cgrcomr  29581  cgrdegen  29588  btwnintr  29603  btwnexch3  29604  btwnouttr  29608  btwnexch  29609  btwndiff  29611  ifscgr  29628  lineid  29667  btwnconn1lem7  29677  btwnconn1lem8  29678  btwnconn1lem9  29679  btwnconn1lem12  29682  midofsegid  29688  brsegle2  29693  btwnoutside  29709  outsideoftr  29713  cnres2  30193  heibor  30251  mzpmfp  30613  mzpmfpOLD  30614  mzpsubst  30615  pellexlem5  30703  pell14qrexpclnn0  30736  pellfundex  30756  qirropth  30778  monotuz  30811  expmordi  30817  congmul  30839  congsub  30842  mzpcong  30844  fzmaxdif  30853  jm2.15nn0  30879  idomsubgmo  31090  fourierdlem42  31778  fourierdlem48  31784  fourierdlem80  31816  lidldomn1  32327  ringccatid  32374  coe1sclmulval  32472  lsmsat  34211  lkrlsp  34305  lkrlsp2  34306  lkrlsp3  34307  lshpkrlem6  34318  latm4  34436  omlspjN  34464  hlatj4  34576  4noncolr3  34655  4noncolr2  34656  4noncolr1  34657  3dimlem3a  34662  3dimlem4a  34665  3dimlem4  34666  3dimlem4OLDN  34667  1cvratex  34675  hlatexch4  34683  3atlem4  34688  atcvrlln2  34721  atcvrlln  34722  llnmlplnN  34741  lplnnlelln  34745  lvoli2  34783  lvolnlelln  34786  lvolnlelpln  34787  4atlem11b  34810  4atlem12b  34813  2lplnj  34822  dalemzeo  34835  dath2  34939  lncvrat  34984  cdlemb  34996  elpaddri  35004  padd4N  35042  llnmod2i2  35065  llnexchb2  35071  dalawlem1  35073  dalawlem2  35074  osumcllem6N  35163  pexmidlem3N  35174  pexmidlem4N  35175  lhp2lt  35203  lhp2at0  35234  lhp2atne  35236  lhp2at0ne  35238  lhpmod2i2  35240  lhpmod6i1  35241  lhpat  35245  lhpat3  35248  4atexlemex6  35276  ltrncoval  35347  ltrncnv  35348  ltrnnidn  35376  cdlemd7  35406  cdleme0b  35414  cdleme0c  35415  cdleme0fN  35420  cdleme0ex1N  35425  cdleme7d  35448  cdleme7e  35449  cdleme7ga  35450  cdleme7  35451  cdleme11a  35462  cdleme17c  35490  cdleme22gb  35496  cdlemeda  35500  cdleme20k  35521  cdleme21a  35527  cdleme21at  35530  cdleme21d  35532  cdleme22f2  35549  cdleme22g  35550  cdleme24  35554  cdleme28  35575  cdlemefrs29cpre1  35600  cdlemefr29exN  35604  cdlemefr32sn2aw  35606  cdleme32fva  35639  cdleme32fva1  35640  cdleme35a  35650  cdleme42c  35674  cdleme42e  35681  cdleme42f  35682  cdleme42g  35683  cdleme42h  35684  cdleme43bN  35692  cdleme46f2g2  35695  cdleme17d2  35697  cdleme4gfv  35709  cdlemeg46c  35715  cdlemeg46nlpq  35719  cdlemeg46gfre  35734  cdlemeg49lebilem  35741  cdleme50trn1  35751  cdleme50trn2  35753  cdleme50ltrn  35759  cdleme  35762  cdlemf1  35763  cdlemf  35765  trlord  35771  ltrniotavalbN  35786  cdlemg1cex  35790  cdlemg2dN  35792  cdlemg2ce  35794  cdlemg2fvlem  35796  cdlemg2idN  35798  cdlemg2kq  35804  cdlemg2l  35805  cdlemg7fvN  35826  cdlemg7aN  35827  cdlemg8a  35829  cdlemg11aq  35840  cdlemg12d  35848  cdlemg13a  35853  cdlemg13  35854  cdlemg14f  35855  cdlemg14g  35856  cdlemg17b  35864  cdlemg27a  35894  cdlemg31b0N  35896  cdlemg31a  35899  cdlemg31b  35900  cdlemg31c  35901  ltrnco  35921  trlcoabs2N  35924  trlcocnvat  35926  trlconid  35927  trlcolem  35928  cdlemg42  35931  cdlemg43  35932  cdlemg47a  35936  cdlemg46  35937  cdlemg47  35938  tendoeq1  35966  tendocoval  35968  tendoco2  35970  tendoplco2  35981  tendopltp  35982  cdlemh1  36017  cdlemh2  36018  cdlemi1  36020  cdlemi  36022  cdlemk1  36033  cdlemk2  36034  cdlemk3  36035  cdlemk4  36036  cdlemk8  36040  cdlemk9  36041  cdlemk9bN  36042  cdlemk31  36098  cdlemk28-3  36110  cdlemk19xlem  36144  cdlemk39u  36170  cdlemk19u  36172  cdlemk56w  36175  cdlemn7  36406  cdlemn8  36407  cdlemn9  36408  dihordlem6  36416  dihordlem7  36417  dihordlem7b  36418  dihord1  36421  dihord2a  36422  dihord11c  36427  dihord2pre  36428  dihord2pre2  36429  dihlsscpre  36437  dihord4  36461  dihord6b  36463  dihmeetlem2N  36502  dihglbcpreN  36503  dihmeetcN  36505  dihmeetbclemN  36507  dihmeetlem3N  36508  dihmeetlem9N  36518  dihmeetlem13N  36522  dihmeetlem20N  36529  mapdpglem24  36907  mapdpglem32  36908  baerlem3lem2  36913  baerlem5alem2  36914  baerlem5blem2  36915  mapdh9aOLDN  36994  hdmap14lem6  37079
  Copyright terms: Public domain W3C validator