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  5492  fsnunf  5923  f1oiso2  6064  omeulem2  6818  uniinqs  6976  unxpdomlem3  7307  fin23lem11  8189  reclem3pr  8918  addid2  9241  dmdcan  9716  xaddass2  10821  xlt2add  10831  xadddi2  10868  expaddzlem  11415  expaddz  11416  expmulz  11418  expdiv  11422  ccatopth2  11769  o1add  12399  o1mul  12400  o1sub  12401  prmexpb  13109  pcpremul  13209  pcdiv  13218  pcqmul  13219  pcqdiv  13223  4sqlem12  13316  f1ocpbllem  13741  ercpbl  13766  erlecpbl  13767  latjlej12  14488  latmlem12  14504  latj4  14522  mndodcong  15172  cmn4  15423  ablsub4  15429  abladdsub4  15430  lsm4  15467  abvdom  15918  abvtrivd  15920  lspsnvs  16178  lspsneu  16187  lspfixed  16192  lspexch  16193  lsmcv  16205  lspsolvlem  16206  mvrf1  16481  coe1sclmulfv  16667  cnprest  17345  isreg2  17433  elptr  17597  hausflimlem  18003  trcfilu  18316  ssblps  18444  ssbl  18445  prdsxmslem2  18551  tgqioo  18823  metnrm  18884  bndth  18975  cph2ass  19167  iscau3  19223  ovolunlem2  19386  dvres2  19791  dvfsumlem2  19903  dvfsum2  19910  deg1tm  20033  plyadd  20128  plymul  20129  coeeu  20136  coemullem  20160  aalioulem4  20244  cxplea  20579  cxple2  20580  cxplt2  20581  cxple2a  20582  cxpcn3lem  20623  angcan  20636  ang180lem5  20647  divsqrsumlem  20810  logexprlim  21001  dchrvmasumlema  21186  dchrisum0lema  21200  logdivsum  21219  log2sumbnd  21230  padicabv  21316  1pthon  21583  chscllem4  23134  mdslmd4i  23828  ofldmul  24231  measxun2  24556  measun  24557  mbfmco2  24607  probun  24669  dedekind  25179  ntrivcvgmul  25222  wsuclem  25568  brbtwn2  25836  axcontlem4  25898  axcontlem8  25902  cgrcomim  25915  cgrcoml  25922  cgrcomr  25923  cgrdegen  25930  btwnintr  25945  btwnexch3  25946  btwnouttr  25950  btwnexch  25951  btwndiff  25953  ifscgr  25970  lineid  26009  btwnconn1lem7  26019  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem12  26024  midofsegid  26030  brsegle2  26035  btwnoutside  26051  outsideoftr  26055  cnres2  26463  heibor  26521  mzpmfp  26795  mzpsubst  26796  pellexlem5  26887  pell14qrexpclnn0  26920  pellfundex  26940  qirropth  26962  monotuz  26995  expmordi  27001  congmul  27023  congsub  27026  mzpcong  27028  fzmaxdif  27037  jm2.15nn0  27065  symgsssg  27376  symgfisg  27377  idomsubgmo  27482  lsmsat  29743  lkrlsp  29837  lkrlsp2  29838  lkrlsp3  29839  lshpkrlem6  29850  latm4  29968  omlspjN  29996  hlatj4  30108  4noncolr3  30187  4noncolr2  30188  4noncolr1  30189  3dimlem3a  30194  3dimlem4a  30197  3dimlem4  30198  3dimlem4OLDN  30199  1cvratex  30207  hlatexch4  30215  3atlem4  30220  atcvrlln2  30253  atcvrlln  30254  llnmlplnN  30273  lplnnlelln  30277  lvoli2  30315  lvolnlelln  30318  lvolnlelpln  30319  4atlem11b  30342  4atlem12b  30345  2lplnj  30354  dalemzeo  30367  dath2  30471  lncvrat  30516  cdlemb  30528  elpaddri  30536  padd4N  30574  llnmod2i2  30597  llnexchb2  30603  dalawlem1  30605  dalawlem2  30606  osumcllem6N  30695  pexmidlem3N  30706  pexmidlem4N  30707  lhp2lt  30735  lhp2at0  30766  lhp2atne  30768  lhp2at0ne  30770  lhpmod2i2  30772  lhpmod6i1  30773  lhpat  30777  lhpat3  30780  4atexlemex6  30808  ltrncoval  30879  ltrncnv  30880  ltrnnidn  30908  cdlemd7  30938  cdleme0b  30946  cdleme0c  30947  cdleme0fN  30952  cdleme0ex1N  30957  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme11a  30994  cdleme17c  31022  cdleme22gb  31028  cdlemeda  31032  cdleme20k  31053  cdleme21a  31059  cdleme21at  31062  cdleme21d  31064  cdleme22f2  31081  cdleme22g  31082  cdleme24  31086  cdleme28  31107  cdlemefrs29cpre1  31132  cdlemefr29exN  31136  cdlemefr32sn2aw  31138  cdleme32fva  31171  cdleme32fva1  31172  cdleme35a  31182  cdleme42c  31206  cdleme42e  31213  cdleme42f  31214  cdleme42g  31215  cdleme42h  31216  cdleme43bN  31224  cdleme46f2g2  31227  cdleme17d2  31229  cdleme4gfv  31241  cdlemeg46c  31247  cdlemeg46nlpq  31251  cdlemeg46gfre  31266  cdlemeg49lebilem  31273  cdleme50trn1  31283  cdleme50trn2  31285  cdleme50ltrn  31291  cdleme  31294  cdlemf1  31295  cdlemf  31297  trlord  31303  ltrniotavalbN  31318  cdlemg1cex  31322  cdlemg2dN  31324  cdlemg2ce  31326  cdlemg2fvlem  31328  cdlemg2idN  31330  cdlemg2kq  31336  cdlemg2l  31337  cdlemg7fvN  31358  cdlemg7aN  31359  cdlemg8a  31361  cdlemg11aq  31372  cdlemg12d  31380  cdlemg13a  31385  cdlemg13  31386  cdlemg14f  31387  cdlemg14g  31388  cdlemg17b  31396  cdlemg27a  31426  cdlemg31b0N  31428  cdlemg31a  31431  cdlemg31b  31432  cdlemg31c  31433  ltrnco  31453  trlcoabs2N  31456  trlcocnvat  31458  trlconid  31459  trlcolem  31460  cdlemg42  31463  cdlemg43  31464  cdlemg47a  31468  cdlemg46  31469  cdlemg47  31470  tendoeq1  31498  tendocoval  31500  tendoco2  31502  tendoplco2  31513  tendopltp  31514  cdlemh1  31549  cdlemh2  31550  cdlemi1  31552  cdlemi  31554  cdlemk1  31565  cdlemk2  31566  cdlemk3  31567  cdlemk4  31568  cdlemk8  31572  cdlemk9  31573  cdlemk9bN  31574  cdlemk31  31630  cdlemk28-3  31642  cdlemk19xlem  31676  cdlemk39u  31702  cdlemk19u  31704  cdlemk56w  31707  cdlemn7  31938  cdlemn8  31939  cdlemn9  31940  dihordlem6  31948  dihordlem7  31949  dihordlem7b  31950  dihord1  31953  dihord2a  31954  dihord11c  31959  dihord2pre  31960  dihord2pre2  31961  dihlsscpre  31969  dihord4  31993  dihord6b  31995  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetcN  32037  dihmeetbclemN  32039  dihmeetlem3N  32040  dihmeetlem9N  32050  dihmeetlem13N  32054  dihmeetlem20N  32061  mapdpglem24  32439  mapdpglem32  32440  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  mapdh9aOLDN  32526  hdmap14lem6  32611
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