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  5301  fsnunf  5718  f1oiso2  5849  omeulem2  6581  unxpdomlem3  7069  fin23lem11  7943  reclem3pr  8673  addid2  8995  dmdcan  9470  xaddass2  10570  xlt2add  10580  xadddi2  10617  expaddzlem  11145  expaddz  11146  expmulz  11148  expdiv  11152  ccatopth2  11463  o1add  12087  o1mul  12088  o1sub  12089  prmexpb  12796  pcpremul  12896  pcdiv  12905  pcqmul  12906  pcqdiv  12910  4sqlem12  13003  f1ocpbllem  13426  ercpbl  13451  erlecpbl  13452  latjlej12  14173  latmlem12  14189  latj4  14207  mndodcong  14857  cmn4  15108  ablsub4  15114  abladdsub4  15115  lsm4  15152  abvdom  15603  abvtrivd  15605  lspsnvs  15867  lspsneu  15876  lspfixed  15881  lspexch  15882  lsmcv  15894  lspsolvlem  15895  mvrf1  16170  coe1sclmulfv  16359  cnprest  17017  isreg2  17105  elptr  17268  hausflimlem  17674  ssbl  17971  prdsxmslem2  18075  tgqioo  18306  metnrm  18366  bndth  18456  cph2ass  18648  iscau3  18704  ovolunlem2  18857  dvres2  19262  dvfsumlem2  19374  dvfsum2  19381  deg1tm  19504  plyadd  19599  plymul  19600  coeeu  19607  coemullem  19631  aalioulem4  19715  cxplea  20043  cxple2  20044  cxplt2  20045  cxple2a  20046  cxpcn3lem  20087  angcan  20100  ang180lem5  20111  divsqrsumlem  20274  logexprlim  20464  dchrvmasumlema  20649  dchrisum0lema  20663  logdivsum  20682  log2sumbnd  20693  padicabv  20779  chscllem4  22219  mdslmd4i  22913  measxun  23539  mbfmco2  23570  dedekind  24082  brbtwn2  24533  axcontlem4  24595  axcontlem8  24599  cgrcomim  24612  cgrcoml  24619  cgrcomr  24620  cgrdegen  24627  btwnintr  24642  btwnexch3  24643  btwnouttr  24647  btwnexch  24648  btwndiff  24650  ifscgr  24667  lineid  24706  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem12  24721  midofsegid  24727  brsegle2  24732  btwnoutside  24748  outsideoftr  24752  uninqs  25039  valcurfn2  25205  oriso  25214  islimrs  25580  islimrs3  25581  islimrs4  25582  icccon4  25702  isepic  25824  rocatval  25959  cnres2  26483  heibor  26545  mzpmfp  26825  mzpsubst  26826  pellexlem5  26918  pell14qrexpclnn0  26951  pellfundex  26971  qirropth  26993  monotuz  27026  expmordi  27032  congmul  27054  congsub  27057  mzpcong  27059  fzmaxdif  27068  jm2.15nn0  27096  symgsssg  27408  symgfisg  27409  idomsubgmo  27514  lsmsat  29198  lkrlsp  29292  lkrlsp2  29293  lkrlsp3  29294  lshpkrlem6  29305  latm4  29423  omlspjN  29451  hlatj4  29563  4noncolr3  29642  4noncolr2  29643  4noncolr1  29644  3dimlem3a  29649  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  1cvratex  29662  hlatexch4  29670  3atlem4  29675  atcvrlln2  29708  atcvrlln  29709  llnmlplnN  29728  lplnnlelln  29732  lvoli2  29770  lvolnlelln  29773  lvolnlelpln  29774  4atlem11b  29797  4atlem12b  29800  2lplnj  29809  dalemzeo  29822  dath2  29926  lncvrat  29971  cdlemb  29983  elpaddri  29991  padd4N  30029  llnmod2i2  30052  llnexchb2  30058  dalawlem1  30060  dalawlem2  30061  osumcllem6N  30150  pexmidlem3N  30161  pexmidlem4N  30162  lhp2lt  30190  lhp2at0  30221  lhp2atne  30223  lhp2at0ne  30225  lhpmod2i2  30227  lhpmod6i1  30228  lhpat  30232  lhpat3  30235  4atexlemex6  30263  ltrncoval  30334  ltrncnv  30335  ltrnnidn  30363  cdlemd7  30393  cdleme0b  30401  cdleme0c  30402  cdleme0fN  30407  cdleme0ex1N  30412  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme11a  30449  cdleme17c  30477  cdleme22gb  30483  cdlemeda  30487  cdleme20k  30508  cdleme21a  30514  cdleme21at  30517  cdleme21d  30519  cdleme22f2  30536  cdleme22g  30537  cdleme24  30541  cdleme28  30562  cdlemefrs29cpre1  30587  cdlemefr29exN  30591  cdlemefr32sn2aw  30593  cdleme32fva  30626  cdleme32fva1  30627  cdleme35a  30637  cdleme42c  30661  cdleme42e  30668  cdleme42f  30669  cdleme42g  30670  cdleme42h  30671  cdleme43bN  30679  cdleme46f2g2  30682  cdleme17d2  30684  cdleme4gfv  30696  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdlemeg46gfre  30721  cdlemeg49lebilem  30728  cdleme50trn1  30738  cdleme50trn2  30740  cdleme50ltrn  30746  cdleme  30749  cdlemf1  30750  cdlemf  30752  trlord  30758  ltrniotavalbN  30773  cdlemg1cex  30777  cdlemg2dN  30779  cdlemg2ce  30781  cdlemg2fvlem  30783  cdlemg2idN  30785  cdlemg2kq  30791  cdlemg2l  30792  cdlemg7fvN  30813  cdlemg7aN  30814  cdlemg8a  30816  cdlemg11aq  30827  cdlemg12d  30835  cdlemg13a  30840  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17b  30851  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg31a  30886  cdlemg31b  30887  cdlemg31c  30888  ltrnco  30908  trlcoabs2N  30911  trlcocnvat  30913  trlconid  30914  trlcolem  30915  cdlemg42  30918  cdlemg43  30919  cdlemg47a  30923  cdlemg46  30924  cdlemg47  30925  tendoeq1  30953  tendocoval  30955  tendoco2  30957  tendoplco2  30968  tendopltp  30969  cdlemh1  31004  cdlemh2  31005  cdlemi1  31007  cdlemi  31009  cdlemk1  31020  cdlemk2  31021  cdlemk3  31022  cdlemk4  31023  cdlemk8  31027  cdlemk9  31028  cdlemk9bN  31029  cdlemk31  31085  cdlemk28-3  31097  cdlemk19xlem  31131  cdlemk39u  31157  cdlemk19u  31159  cdlemk56w  31162  cdlemn7  31393  cdlemn8  31394  cdlemn9  31395  dihordlem6  31403  dihordlem7  31404  dihordlem7b  31405  dihord1  31408  dihord2a  31409  dihord11c  31414  dihord2pre  31415  dihord2pre2  31416  dihlsscpre  31424  dihord4  31448  dihord6b  31450  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetcN  31492  dihmeetbclemN  31494  dihmeetlem3N  31495  dihmeetlem9N  31505  dihmeetlem13N  31509  dihmeetlem20N  31516  mapdpglem24  31894  mapdpglem32  31895  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  mapdh9aOLDN  31981  hdmap14lem6  32066
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