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

Theorem simp2r 984
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl2r  1011  simpr2r  1017  simp12r  1071  simp22r  1077  simp32r  1083  funprg  5500  fsnunf  5931  f1oiso2  6072  omeulem2  6826  uniinqs  6984  unxpdomlem3  7315  fin23lem11  8197  reclem3pr  8926  addid2  9249  dmdcan  9724  xaddass2  10829  xlt2add  10839  xadddi2  10876  expaddzlem  11423  expaddz  11424  expmulz  11426  expdiv  11430  ccatopth2  11777  o1add  12407  o1mul  12408  o1sub  12409  prmexpb  13117  pcpremul  13217  pcdiv  13226  pcqmul  13227  pcqdiv  13231  4sqlem12  13324  f1ocpbllem  13749  ercpbl  13774  erlecpbl  13775  latjlej12  14496  latmlem12  14512  latj4  14530  mndodcong  15180  cmn4  15431  ablsub4  15437  abladdsub4  15438  lsm4  15475  abvdom  15926  abvtrivd  15928  lspsnvs  16186  lspsneu  16195  lspfixed  16200  lspexch  16201  lsmcv  16213  lspsolvlem  16214  mvrf1  16489  coe1sclmulfv  16675  cnprest  17353  isreg2  17441  elptr  17605  hausflimlem  18011  trcfilu  18324  ssblps  18452  ssbl  18453  prdsxmslem2  18559  tgqioo  18831  metnrm  18892  bndth  18983  cph2ass  19175  iscau3  19231  ovolunlem2  19394  dvres2  19799  dvfsumlem2  19911  dvfsum2  19918  deg1tm  20041  plyadd  20136  plymul  20137  coeeu  20144  coemullem  20168  aalioulem4  20252  cxplea  20587  cxple2  20588  cxplt2  20589  cxple2a  20590  cxpcn3lem  20631  angcan  20644  ang180lem5  20655  divsqrsumlem  20818  logexprlim  21009  dchrvmasumlema  21194  dchrisum0lema  21208  logdivsum  21227  log2sumbnd  21238  padicabv  21324  1pthon  21591  chscllem4  23142  mdslmd4i  23836  ofldmul  24239  measxun2  24564  measun  24565  mbfmco2  24615  probun  24677  dedekind  25187  ntrivcvgmul  25230  wsuclem  25576  brbtwn2  25844  axcontlem4  25906  axcontlem8  25910  cgrcomim  25923  cgrcoml  25930  cgrcomr  25931  cgrdegen  25938  btwnintr  25953  btwnexch3  25954  btwnouttr  25958  btwnexch  25959  btwndiff  25961  ifscgr  25978  lineid  26017  btwnconn1lem7  26027  btwnconn1lem8  26028  btwnconn1lem9  26029  btwnconn1lem12  26032  midofsegid  26038  brsegle2  26043  btwnoutside  26059  outsideoftr  26063  cnres2  26472  heibor  26530  mzpmfp  26804  mzpsubst  26805  pellexlem5  26896  pell14qrexpclnn0  26929  pellfundex  26949  qirropth  26971  monotuz  27004  expmordi  27010  congmul  27032  congsub  27035  mzpcong  27037  fzmaxdif  27046  jm2.15nn0  27074  symgsssg  27385  symgfisg  27386  idomsubgmo  27491  lsmsat  29806  lkrlsp  29900  lkrlsp2  29901  lkrlsp3  29902  lshpkrlem6  29913  latm4  30031  omlspjN  30059  hlatj4  30171  4noncolr3  30250  4noncolr2  30251  4noncolr1  30252  3dimlem3a  30257  3dimlem4a  30260  3dimlem4  30261  3dimlem4OLDN  30262  1cvratex  30270  hlatexch4  30278  3atlem4  30283  atcvrlln2  30316  atcvrlln  30317  llnmlplnN  30336  lplnnlelln  30340  lvoli2  30378  lvolnlelln  30381  lvolnlelpln  30382  4atlem11b  30405  4atlem12b  30408  2lplnj  30417  dalemzeo  30430  dath2  30534  lncvrat  30579  cdlemb  30591  elpaddri  30599  padd4N  30637  llnmod2i2  30660  llnexchb2  30666  dalawlem1  30668  dalawlem2  30669  osumcllem6N  30758  pexmidlem3N  30769  pexmidlem4N  30770  lhp2lt  30798  lhp2at0  30829  lhp2atne  30831  lhp2at0ne  30833  lhpmod2i2  30835  lhpmod6i1  30836  lhpat  30840  lhpat3  30843  4atexlemex6  30871  ltrncoval  30942  ltrncnv  30943  ltrnnidn  30971  cdlemd7  31001  cdleme0b  31009  cdleme0c  31010  cdleme0fN  31015  cdleme0ex1N  31020  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme7  31046  cdleme11a  31057  cdleme17c  31085  cdleme22gb  31091  cdlemeda  31095  cdleme20k  31116  cdleme21a  31122  cdleme21at  31125  cdleme21d  31127  cdleme22f2  31144  cdleme22g  31145  cdleme24  31149  cdleme28  31170  cdlemefrs29cpre1  31195  cdlemefr29exN  31199  cdlemefr32sn2aw  31201  cdleme32fva  31234  cdleme32fva1  31235  cdleme35a  31245  cdleme42c  31269  cdleme42e  31276  cdleme42f  31277  cdleme42g  31278  cdleme42h  31279  cdleme43bN  31287  cdleme46f2g2  31290  cdleme17d2  31292  cdleme4gfv  31304  cdlemeg46c  31310  cdlemeg46nlpq  31314  cdlemeg46gfre  31329  cdlemeg49lebilem  31336  cdleme50trn1  31346  cdleme50trn2  31348  cdleme50ltrn  31354  cdleme  31357  cdlemf1  31358  cdlemf  31360  trlord  31366  ltrniotavalbN  31381  cdlemg1cex  31385  cdlemg2dN  31387  cdlemg2ce  31389  cdlemg2fvlem  31391  cdlemg2idN  31393  cdlemg2kq  31399  cdlemg2l  31400  cdlemg7fvN  31421  cdlemg7aN  31422  cdlemg8a  31424  cdlemg11aq  31435  cdlemg12d  31443  cdlemg13a  31448  cdlemg13  31449  cdlemg14f  31450  cdlemg14g  31451  cdlemg17b  31459  cdlemg27a  31489  cdlemg31b0N  31491  cdlemg31a  31494  cdlemg31b  31495  cdlemg31c  31496  ltrnco  31516  trlcoabs2N  31519  trlcocnvat  31521  trlconid  31522  trlcolem  31523  cdlemg42  31526  cdlemg43  31527  cdlemg47a  31531  cdlemg46  31532  cdlemg47  31533  tendoeq1  31561  tendocoval  31563  tendoco2  31565  tendoplco2  31576  tendopltp  31577  cdlemh1  31612  cdlemh2  31613  cdlemi1  31615  cdlemi  31617  cdlemk1  31628  cdlemk2  31629  cdlemk3  31630  cdlemk4  31631  cdlemk8  31635  cdlemk9  31636  cdlemk9bN  31637  cdlemk31  31693  cdlemk28-3  31705  cdlemk19xlem  31739  cdlemk39u  31765  cdlemk19u  31767  cdlemk56w  31770  cdlemn7  32001  cdlemn8  32002  cdlemn9  32003  dihordlem6  32011  dihordlem7  32012  dihordlem7b  32013  dihord1  32016  dihord2a  32017  dihord11c  32022  dihord2pre  32023  dihord2pre2  32024  dihlsscpre  32032  dihord4  32056  dihord6b  32058  dihmeetlem2N  32097  dihglbcpreN  32098  dihmeetcN  32100  dihmeetbclemN  32102  dihmeetlem3N  32103  dihmeetlem9N  32113  dihmeetlem13N  32117  dihmeetlem20N  32124  mapdpglem24  32502  mapdpglem32  32503  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  mapdh9aOLDN  32589  hdmap14lem6  32674
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator