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

Theorem simp2r 982
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 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl2r  1009  simpr2r  1015  simp12r  1069  simp22r  1075  simp32r  1081  funprg  5317  fsnunf  5734  f1oiso2  5865  omeulem2  6597  unxpdomlem3  7085  fin23lem11  7959  reclem3pr  8689  addid2  9011  dmdcan  9486  xaddass2  10586  xlt2add  10596  xadddi2  10633  expaddzlem  11161  expaddz  11162  expmulz  11164  expdiv  11168  ccatopth2  11479  o1add  12103  o1mul  12104  o1sub  12105  prmexpb  12812  pcpremul  12912  pcdiv  12921  pcqmul  12922  pcqdiv  12926  4sqlem12  13019  f1ocpbllem  13442  ercpbl  13467  erlecpbl  13468  latjlej12  14189  latmlem12  14205  latj4  14223  mndodcong  14873  cmn4  15124  ablsub4  15130  abladdsub4  15131  lsm4  15168  abvdom  15619  abvtrivd  15621  lspsnvs  15883  lspsneu  15892  lspfixed  15897  lspexch  15898  lsmcv  15910  lspsolvlem  15911  mvrf1  16186  coe1sclmulfv  16375  cnprest  17033  isreg2  17121  elptr  17284  hausflimlem  17690  ssbl  17987  prdsxmslem2  18091  tgqioo  18322  metnrm  18382  bndth  18472  cph2ass  18664  iscau3  18720  ovolunlem2  18873  dvres2  19278  dvfsumlem2  19390  dvfsum2  19397  deg1tm  19520  plyadd  19615  plymul  19616  coeeu  19623  coemullem  19647  aalioulem4  19731  cxplea  20059  cxple2  20060  cxplt2  20061  cxple2a  20062  cxpcn3lem  20103  angcan  20116  ang180lem5  20127  divsqrsumlem  20290  logexprlim  20480  dchrvmasumlema  20665  dchrisum0lema  20679  logdivsum  20698  log2sumbnd  20709  padicabv  20795  chscllem4  22235  mdslmd4i  22929  measxun  23554  mbfmco2  23585  dedekind  24097  brbtwn2  24605  axcontlem4  24667  axcontlem8  24671  cgrcomim  24684  cgrcoml  24691  cgrcomr  24692  cgrdegen  24699  btwnintr  24714  btwnexch3  24715  btwnouttr  24719  btwnexch  24720  btwndiff  24722  ifscgr  24739  lineid  24778  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem12  24793  midofsegid  24799  brsegle2  24804  btwnoutside  24820  outsideoftr  24824  uninqs  25142  valcurfn2  25308  oriso  25317  islimrs  25683  islimrs3  25684  islimrs4  25685  icccon4  25805  isepic  25927  rocatval  26062  cnres2  26586  heibor  26648  mzpmfp  26928  mzpsubst  26929  pellexlem5  27021  pell14qrexpclnn0  27054  pellfundex  27074  qirropth  27096  monotuz  27129  expmordi  27135  congmul  27157  congsub  27160  mzpcong  27162  fzmaxdif  27171  jm2.15nn0  27199  symgsssg  27511  symgfisg  27512  idomsubgmo  27617  lsmsat  29820  lkrlsp  29914  lkrlsp2  29915  lkrlsp3  29916  lshpkrlem6  29927  latm4  30045  omlspjN  30073  hlatj4  30185  4noncolr3  30264  4noncolr2  30265  4noncolr1  30266  3dimlem3a  30271  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  1cvratex  30284  hlatexch4  30292  3atlem4  30297  atcvrlln2  30330  atcvrlln  30331  llnmlplnN  30350  lplnnlelln  30354  lvoli2  30392  lvolnlelln  30395  lvolnlelpln  30396  4atlem11b  30419  4atlem12b  30422  2lplnj  30431  dalemzeo  30444  dath2  30548  lncvrat  30593  cdlemb  30605  elpaddri  30613  padd4N  30651  llnmod2i2  30674  llnexchb2  30680  dalawlem1  30682  dalawlem2  30683  osumcllem6N  30772  pexmidlem3N  30783  pexmidlem4N  30784  lhp2lt  30812  lhp2at0  30843  lhp2atne  30845  lhp2at0ne  30847  lhpmod2i2  30849  lhpmod6i1  30850  lhpat  30854  lhpat3  30857  4atexlemex6  30885  ltrncoval  30956  ltrncnv  30957  ltrnnidn  30985  cdlemd7  31015  cdleme0b  31023  cdleme0c  31024  cdleme0fN  31029  cdleme0ex1N  31034  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11a  31071  cdleme17c  31099  cdleme22gb  31105  cdlemeda  31109  cdleme20k  31130  cdleme21a  31136  cdleme21at  31139  cdleme21d  31141  cdleme22f2  31158  cdleme22g  31159  cdleme24  31163  cdleme28  31184  cdlemefrs29cpre1  31209  cdlemefr29exN  31213  cdlemefr32sn2aw  31215  cdleme32fva  31248  cdleme32fva1  31249  cdleme35a  31259  cdleme42c  31283  cdleme42e  31290  cdleme42f  31291  cdleme42g  31292  cdleme42h  31293  cdleme43bN  31301  cdleme46f2g2  31304  cdleme17d2  31306  cdleme4gfv  31318  cdlemeg46c  31324  cdlemeg46nlpq  31328  cdlemeg46gfre  31343  cdlemeg49lebilem  31350  cdleme50trn1  31360  cdleme50trn2  31362  cdleme50ltrn  31368  cdleme  31371  cdlemf1  31372  cdlemf  31374  trlord  31380  ltrniotavalbN  31395  cdlemg1cex  31399  cdlemg2dN  31401  cdlemg2ce  31403  cdlemg2fvlem  31405  cdlemg2idN  31407  cdlemg2kq  31413  cdlemg2l  31414  cdlemg7fvN  31435  cdlemg7aN  31436  cdlemg8a  31438  cdlemg11aq  31449  cdlemg12d  31457  cdlemg13a  31462  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17b  31473  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg31a  31508  cdlemg31b  31509  cdlemg31c  31510  ltrnco  31530  trlcoabs2N  31533  trlcocnvat  31535  trlconid  31536  trlcolem  31537  cdlemg42  31540  cdlemg43  31541  cdlemg47a  31545  cdlemg46  31546  cdlemg47  31547  tendoeq1  31575  tendocoval  31577  tendoco2  31579  tendoplco2  31590  tendopltp  31591  cdlemh1  31626  cdlemh2  31627  cdlemi1  31629  cdlemi  31631  cdlemk1  31642  cdlemk2  31643  cdlemk3  31644  cdlemk4  31645  cdlemk8  31649  cdlemk9  31650  cdlemk9bN  31651  cdlemk31  31707  cdlemk28-3  31719  cdlemk19xlem  31753  cdlemk39u  31779  cdlemk19u  31781  cdlemk56w  31784  cdlemn7  32015  cdlemn8  32016  cdlemn9  32017  dihordlem6  32025  dihordlem7  32026  dihordlem7b  32027  dihord1  32030  dihord2a  32031  dihord11c  32036  dihord2pre  32037  dihord2pre2  32038  dihlsscpre  32046  dihord4  32070  dihord6b  32072  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbclemN  32116  dihmeetlem3N  32117  dihmeetlem9N  32127  dihmeetlem13N  32131  dihmeetlem20N  32138  mapdpglem24  32516  mapdpglem32  32517  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  mapdh9aOLDN  32603  hdmap14lem6  32688
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator