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

Theorem simp2r 985
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 449 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 980 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpl2r  1012  simpr2r  1018  simp12r  1072  simp22r  1078  simp32r  1084  funprg  5503  fsnunf  5934  f1oiso2  6075  omeulem2  6829  uniinqs  6987  unxpdomlem3  7318  fin23lem11  8202  reclem3pr  8931  addid2  9254  dmdcan  9729  xaddass2  10834  xlt2add  10844  xadddi2  10881  expaddzlem  11428  expaddz  11429  expmulz  11431  expdiv  11435  ccatopth2  11782  o1add  12412  o1mul  12413  o1sub  12414  prmexpb  13122  pcpremul  13222  pcdiv  13231  pcqmul  13232  pcqdiv  13236  4sqlem12  13329  f1ocpbllem  13754  ercpbl  13779  erlecpbl  13780  latjlej12  14501  latmlem12  14517  latj4  14535  mndodcong  15185  cmn4  15436  ablsub4  15442  abladdsub4  15443  lsm4  15480  abvdom  15931  abvtrivd  15933  lspsnvs  16191  lspsneu  16200  lspfixed  16205  lspexch  16206  lsmcv  16218  lspsolvlem  16219  mvrf1  16494  coe1sclmulfv  16680  cnprest  17358  isreg2  17446  elptr  17610  hausflimlem  18016  trcfilu  18329  ssblps  18457  ssbl  18458  prdsxmslem2  18564  tgqioo  18836  metnrm  18897  bndth  18988  cph2ass  19180  iscau3  19236  ovolunlem2  19399  dvres2  19804  dvfsumlem2  19916  dvfsum2  19923  deg1tm  20046  plyadd  20141  plymul  20142  coeeu  20149  coemullem  20173  aalioulem4  20257  cxplea  20592  cxple2  20593  cxplt2  20594  cxple2a  20595  cxpcn3lem  20636  angcan  20649  ang180lem5  20660  divsqrsumlem  20823  logexprlim  21014  dchrvmasumlema  21199  dchrisum0lema  21213  logdivsum  21232  log2sumbnd  21243  padicabv  21329  1pthon  21596  chscllem4  23147  mdslmd4i  23841  ofldmul  24244  measxun2  24569  measun  24570  mbfmco2  24620  probun  24682  dedekind  25192  ntrivcvgmul  25235  wsuclem  25581  brbtwn2  25849  axcontlem4  25911  axcontlem8  25915  cgrcomim  25928  cgrcoml  25935  cgrcomr  25936  cgrdegen  25943  btwnintr  25958  btwnexch3  25959  btwnouttr  25963  btwnexch  25964  btwndiff  25966  ifscgr  25983  lineid  26022  btwnconn1lem7  26032  btwnconn1lem8  26033  btwnconn1lem9  26034  btwnconn1lem12  26037  midofsegid  26043  brsegle2  26048  btwnoutside  26064  outsideoftr  26068  cnres2  26486  heibor  26544  mzpmfp  26818  mzpsubst  26819  pellexlem5  26910  pell14qrexpclnn0  26943  pellfundex  26963  qirropth  26985  monotuz  27018  expmordi  27024  congmul  27046  congsub  27049  mzpcong  27051  fzmaxdif  27060  jm2.15nn0  27088  symgsssg  27399  symgfisg  27400  idomsubgmo  27505  lsmsat  29880  lkrlsp  29974  lkrlsp2  29975  lkrlsp3  29976  lshpkrlem6  29987  latm4  30105  omlspjN  30133  hlatj4  30245  4noncolr3  30324  4noncolr2  30325  4noncolr1  30326  3dimlem3a  30331  3dimlem4a  30334  3dimlem4  30335  3dimlem4OLDN  30336  1cvratex  30344  hlatexch4  30352  3atlem4  30357  atcvrlln2  30390  atcvrlln  30391  llnmlplnN  30410  lplnnlelln  30414  lvoli2  30452  lvolnlelln  30455  lvolnlelpln  30456  4atlem11b  30479  4atlem12b  30482  2lplnj  30491  dalemzeo  30504  dath2  30608  lncvrat  30653  cdlemb  30665  elpaddri  30673  padd4N  30711  llnmod2i2  30734  llnexchb2  30740  dalawlem1  30742  dalawlem2  30743  osumcllem6N  30832  pexmidlem3N  30843  pexmidlem4N  30844  lhp2lt  30872  lhp2at0  30903  lhp2atne  30905  lhp2at0ne  30907  lhpmod2i2  30909  lhpmod6i1  30910  lhpat  30914  lhpat3  30917  4atexlemex6  30945  ltrncoval  31016  ltrncnv  31017  ltrnnidn  31045  cdlemd7  31075  cdleme0b  31083  cdleme0c  31084  cdleme0fN  31089  cdleme0ex1N  31094  cdleme7d  31117  cdleme7e  31118  cdleme7ga  31119  cdleme7  31120  cdleme11a  31131  cdleme17c  31159  cdleme22gb  31165  cdlemeda  31169  cdleme20k  31190  cdleme21a  31196  cdleme21at  31199  cdleme21d  31201  cdleme22f2  31218  cdleme22g  31219  cdleme24  31223  cdleme28  31244  cdlemefrs29cpre1  31269  cdlemefr29exN  31273  cdlemefr32sn2aw  31275  cdleme32fva  31308  cdleme32fva1  31309  cdleme35a  31319  cdleme42c  31343  cdleme42e  31350  cdleme42f  31351  cdleme42g  31352  cdleme42h  31353  cdleme43bN  31361  cdleme46f2g2  31364  cdleme17d2  31366  cdleme4gfv  31378  cdlemeg46c  31384  cdlemeg46nlpq  31388  cdlemeg46gfre  31403  cdlemeg49lebilem  31410  cdleme50trn1  31420  cdleme50trn2  31422  cdleme50ltrn  31428  cdleme  31431  cdlemf1  31432  cdlemf  31434  trlord  31440  ltrniotavalbN  31455  cdlemg1cex  31459  cdlemg2dN  31461  cdlemg2ce  31463  cdlemg2fvlem  31465  cdlemg2idN  31467  cdlemg2kq  31473  cdlemg2l  31474  cdlemg7fvN  31495  cdlemg7aN  31496  cdlemg8a  31498  cdlemg11aq  31509  cdlemg12d  31517  cdlemg13a  31522  cdlemg13  31523  cdlemg14f  31524  cdlemg14g  31525  cdlemg17b  31533  cdlemg27a  31563  cdlemg31b0N  31565  cdlemg31a  31568  cdlemg31b  31569  cdlemg31c  31570  ltrnco  31590  trlcoabs2N  31593  trlcocnvat  31595  trlconid  31596  trlcolem  31597  cdlemg42  31600  cdlemg43  31601  cdlemg47a  31605  cdlemg46  31606  cdlemg47  31607  tendoeq1  31635  tendocoval  31637  tendoco2  31639  tendoplco2  31650  tendopltp  31651  cdlemh1  31686  cdlemh2  31687  cdlemi1  31689  cdlemi  31691  cdlemk1  31702  cdlemk2  31703  cdlemk3  31704  cdlemk4  31705  cdlemk8  31709  cdlemk9  31710  cdlemk9bN  31711  cdlemk31  31767  cdlemk28-3  31779  cdlemk19xlem  31813  cdlemk39u  31839  cdlemk19u  31841  cdlemk56w  31844  cdlemn7  32075  cdlemn8  32076  cdlemn9  32077  dihordlem6  32085  dihordlem7  32086  dihordlem7b  32087  dihord1  32090  dihord2a  32091  dihord11c  32096  dihord2pre  32097  dihord2pre2  32098  dihlsscpre  32106  dihord4  32130  dihord6b  32132  dihmeetlem2N  32171  dihglbcpreN  32172  dihmeetcN  32174  dihmeetbclemN  32176  dihmeetlem3N  32177  dihmeetlem9N  32187  dihmeetlem13N  32191  dihmeetlem20N  32198  mapdpglem24  32576  mapdpglem32  32577  baerlem3lem2  32582  baerlem5alem2  32583  baerlem5blem2  32584  mapdh9aOLDN  32663  hdmap14lem6  32748
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator