MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2r 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  5440  fsnunf  5870  f1oiso2  6011  omeulem2  6762  uniinqs  6920  unxpdomlem3  7251  fin23lem11  8130  reclem3pr  8859  addid2  9181  dmdcan  9656  xaddass2  10761  xlt2add  10771  xadddi2  10808  expaddzlem  11350  expaddz  11351  expmulz  11353  expdiv  11357  ccatopth2  11704  o1add  12334  o1mul  12335  o1sub  12336  prmexpb  13044  pcpremul  13144  pcdiv  13153  pcqmul  13154  pcqdiv  13158  4sqlem12  13251  f1ocpbllem  13676  ercpbl  13701  erlecpbl  13702  latjlej12  14423  latmlem12  14439  latj4  14457  mndodcong  15107  cmn4  15358  ablsub4  15364  abladdsub4  15365  lsm4  15402  abvdom  15853  abvtrivd  15855  lspsnvs  16113  lspsneu  16122  lspfixed  16127  lspexch  16128  lsmcv  16140  lspsolvlem  16141  mvrf1  16416  coe1sclmulfv  16602  cnprest  17275  isreg2  17363  elptr  17526  hausflimlem  17932  trcfilu  18245  ssbl  18345  prdsxmslem2  18449  tgqioo  18702  metnrm  18763  bndth  18854  cph2ass  19046  iscau3  19102  ovolunlem2  19261  dvres2  19666  dvfsumlem2  19778  dvfsum2  19785  deg1tm  19908  plyadd  20003  plymul  20004  coeeu  20011  coemullem  20035  aalioulem4  20119  cxplea  20454  cxple2  20455  cxplt2  20456  cxple2a  20457  cxpcn3lem  20498  angcan  20511  ang180lem5  20522  divsqrsumlem  20685  logexprlim  20876  dchrvmasumlema  21061  dchrisum0lema  21075  logdivsum  21094  log2sumbnd  21105  padicabv  21191  1pthon  21439  chscllem4  22990  mdslmd4i  23684  ofldmul  24065  measxun2  24358  measun  24359  mbfmco2  24409  probun  24456  dedekind  24966  ntrivcvgmul  25009  brbtwn2  25558  axcontlem4  25620  axcontlem8  25624  cgrcomim  25637  cgrcoml  25644  cgrcomr  25645  cgrdegen  25652  btwnintr  25667  btwnexch3  25668  btwnouttr  25672  btwnexch  25673  btwndiff  25675  ifscgr  25692  lineid  25731  btwnconn1lem7  25741  btwnconn1lem8  25742  btwnconn1lem9  25743  btwnconn1lem12  25746  midofsegid  25752  brsegle2  25757  btwnoutside  25773  outsideoftr  25777  cnres2  26163  heibor  26221  mzpmfp  26495  mzpsubst  26496  pellexlem5  26587  pell14qrexpclnn0  26620  pellfundex  26640  qirropth  26662  monotuz  26695  expmordi  26701  congmul  26723  congsub  26726  mzpcong  26728  fzmaxdif  26737  jm2.15nn0  26765  symgsssg  27077  symgfisg  27078  idomsubgmo  27183  lsmsat  29123  lkrlsp  29217  lkrlsp2  29218  lkrlsp3  29219  lshpkrlem6  29230  latm4  29348  omlspjN  29376  hlatj4  29488  4noncolr3  29567  4noncolr2  29568  4noncolr1  29569  3dimlem3a  29574  3dimlem4a  29577  3dimlem4  29578  3dimlem4OLDN  29579  1cvratex  29587  hlatexch4  29595  3atlem4  29600  atcvrlln2  29633  atcvrlln  29634  llnmlplnN  29653  lplnnlelln  29657  lvoli2  29695  lvolnlelln  29698  lvolnlelpln  29699  4atlem11b  29722  4atlem12b  29725  2lplnj  29734  dalemzeo  29747  dath2  29851  lncvrat  29896  cdlemb  29908  elpaddri  29916  padd4N  29954  llnmod2i2  29977  llnexchb2  29983  dalawlem1  29985  dalawlem2  29986  osumcllem6N  30075  pexmidlem3N  30086  pexmidlem4N  30087  lhp2lt  30115  lhp2at0  30146  lhp2atne  30148  lhp2at0ne  30150  lhpmod2i2  30152  lhpmod6i1  30153  lhpat  30157  lhpat3  30160  4atexlemex6  30188  ltrncoval  30259  ltrncnv  30260  ltrnnidn  30288  cdlemd7  30318  cdleme0b  30326  cdleme0c  30327  cdleme0fN  30332  cdleme0ex1N  30337  cdleme7d  30360  cdleme7e  30361  cdleme7ga  30362  cdleme7  30363  cdleme11a  30374  cdleme17c  30402  cdleme22gb  30408  cdlemeda  30412  cdleme20k  30433  cdleme21a  30439  cdleme21at  30442  cdleme21d  30444  cdleme22f2  30461  cdleme22g  30462  cdleme24  30466  cdleme28  30487  cdlemefrs29cpre1  30512  cdlemefr29exN  30516  cdlemefr32sn2aw  30518  cdleme32fva  30551  cdleme32fva1  30552  cdleme35a  30562  cdleme42c  30586  cdleme42e  30593  cdleme42f  30594  cdleme42g  30595  cdleme42h  30596  cdleme43bN  30604  cdleme46f2g2  30607  cdleme17d2  30609  cdleme4gfv  30621  cdlemeg46c  30627  cdlemeg46nlpq  30631  cdlemeg46gfre  30646  cdlemeg49lebilem  30653  cdleme50trn1  30663  cdleme50trn2  30665  cdleme50ltrn  30671  cdleme  30674  cdlemf1  30675  cdlemf  30677  trlord  30683  ltrniotavalbN  30698  cdlemg1cex  30702  cdlemg2dN  30704  cdlemg2ce  30706  cdlemg2fvlem  30708  cdlemg2idN  30710  cdlemg2kq  30716  cdlemg2l  30717  cdlemg7fvN  30738  cdlemg7aN  30739  cdlemg8a  30741  cdlemg11aq  30752  cdlemg12d  30760  cdlemg13a  30765  cdlemg13  30766  cdlemg14f  30767  cdlemg14g  30768  cdlemg17b  30776  cdlemg27a  30806  cdlemg31b0N  30808  cdlemg31a  30811  cdlemg31b  30812  cdlemg31c  30813  ltrnco  30833  trlcoabs2N  30836  trlcocnvat  30838  trlconid  30839  trlcolem  30840  cdlemg42  30843  cdlemg43  30844  cdlemg47a  30848  cdlemg46  30849  cdlemg47  30850  tendoeq1  30878  tendocoval  30880  tendoco2  30882  tendoplco2  30893  tendopltp  30894  cdlemh1  30929  cdlemh2  30930  cdlemi1  30932  cdlemi  30934  cdlemk1  30945  cdlemk2  30946  cdlemk3  30947  cdlemk4  30948  cdlemk8  30952  cdlemk9  30953  cdlemk9bN  30954  cdlemk31  31010  cdlemk28-3  31022  cdlemk19xlem  31056  cdlemk39u  31082  cdlemk19u  31084  cdlemk56w  31087  cdlemn7  31318  cdlemn8  31319  cdlemn9  31320  dihordlem6  31328  dihordlem7  31329  dihordlem7b  31330  dihord1  31333  dihord2a  31334  dihord11c  31339  dihord2pre  31340  dihord2pre2  31341  dihlsscpre  31349  dihord4  31373  dihord6b  31375  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetcN  31417  dihmeetbclemN  31419  dihmeetlem3N  31420  dihmeetlem9N  31430  dihmeetlem13N  31434  dihmeetlem20N  31441  mapdpglem24  31819  mapdpglem32  31820  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827  mapdh9aOLDN  31906  hdmap14lem6  31991
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