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

Theorem simp2l 983
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2l  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl2l  1010  simpr2l  1016  simp12l  1070  simp22l  1076  simp32l  1082  funprg  5492  fsnunf  5923  f1oiso2  6064  omeulem2  6818  uniinqs  6976  unxpdomlem3  7307  gruina  8685  addid2  9241  dmdcan  9716  xaddass  10820  xaddass2  10821  xlt2add  10831  xmulasslem3  10857  xadddi2  10868  xadddi2r  10869  expaddzlem  11415  expaddz  11416  expmulz  11418  expdiv  11422  modexp  11506  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  latj4rot  14523  mndodcong  15172  cmn4  15423  ablsub4  15429  abladdsub4  15430  lsm4  15467  abvdom  15918  abvres  15919  abvtrivd  15920  lspsnvs  16178  lspsneu  16187  lspfixed  16192  lspexch  16193  lsmcv  16205  lspsolvlem  16206  coe1sclmulfv  16667  cnprest  17345  hausnei2  17409  isreg2  17433  cmpcld  17457  llyrest  17540  nllyrest  17541  elptr  17597  basqtop  17735  hausflimlem  18003  tmdgsum  18117  utop2nei  18272  trcfilu  18316  ssblps  18444  ssbl  18445  prdsxmslem2  18551  tgqioo  18823  metnrm  18884  bndth  18975  cph2ass  19167  lmmbr2  19204  iscau3  19223  bcthlem5  19273  ovolunlem2  19386  dvres2  19791  dvfsumlem2  19903  plyadd  20128  plymul  20129  coeeu  20136  coemullem  20160  aalioulem4  20244  mulcxp  20568  cxplea  20579  cxple2  20580  cxplt2  20581  cxpcn3lem  20623  angcan  20636  ang180lem5  20647  divsqrsumlem  20810  logexprlim  21001  dchrvmasumlema  21186  dchrisum0lema  21200  logdivsum  21219  log2sumbnd  21230  abvcxp  21301  padicabv  21316  1pthon  21583  gxmodid  21859  chscllem4  23134  measxun2  24556  measun  24557  mbfmco2  24607  probun  24669  dedekind  25179  ntrivcvgmul  25222  nofulllem5  25653  brbtwn2  25836  axcontlem4  25898  axcontlem8  25902  cgrcomim  25915  cgrcoml  25922  cgrcomr  25923  cgrdegen  25930  btwnintr  25945  btwnexch3  25946  btwnouttr2  25948  btwnouttr  25950  btwnexch  25951  btwndiff  25953  lineid  26009  idinside  26010  btwnconn1lem7  26019  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem12  26024  btwnconn1lem14  26026  btwnconn3  26029  midofsegid  26030  segcon2  26031  brsegle2  26035  btwnoutside  26051  outsideoftr  26055  outsideofeu  26057  linethru  26079  cnres2  26463  heibor  26521  mzpsubst  26796  pellexlem5  26887  pellex  26889  pell14qrexpclnn0  26920  pellfundex  26940  qirropth  26962  monotuz  26995  expmordi  27001  congtr  27021  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  latm4  29968  omlspjN  29996  hlatj4  30108  4noncolr3  30187  4noncolr2  30188  4noncolr1  30189  athgt  30190  3dimlem3a  30194  3dimlem4a  30197  3dimlem4  30198  3dimlem4OLDN  30199  3dim3  30203  1cvratex  30207  hlatexch4  30215  3atlem4  30220  atcvrlln2  30253  atcvrlln  30254  lplnnlelln  30277  lvoli2  30315  lvolnlelln  30318  lvolnlelpln  30319  4atlem11b  30342  4atlem12b  30345  2lplnja  30353  2lplnj  30354  dalemyeo  30366  dath2  30471  lncvrat  30516  cdlemblem  30527  cdlemb  30528  elpaddri  30536  padd4N  30574  llnmod2i2  30597  llnexchb2  30603  dalawlem1  30605  dalawlem2  30606  pclfinN  30634  osumcllem6N  30695  pexmidlem3N  30706  lhp2lt  30735  lhp2at0  30766  lhp2atnle  30767  lhp2atne  30768  lhp2at0nle  30769  lhp2at0ne  30770  lhpelim  30771  lhpmod2i2  30772  lhpmod6i1  30773  lhple  30776  lhpat  30777  lhpat3  30780  ltrncoelN  30877  ltrncoat  30878  ltrncnv  30880  trlat  30903  trl0  30904  ltrnnidn  30908  trlnid  30913  cdlemd7  30938  cdleme0b  30946  cdleme0c  30947  cdleme0fN  30952  cdleme02N  30956  cdleme0ex1N  30957  cdleme0ex2N  30958  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme8  30984  cdleme11a  30994  cdleme17c  31022  cdleme22gb  31028  cdlemeda  31032  cdleme20k  31053  cdleme21a  31059  cdleme21d  31064  cdleme22f2  31081  cdleme22g  31082  cdleme23a  31083  cdleme23b  31084  cdleme23c  31085  cdleme24  31086  cdleme28  31107  cdlemefrs32fva1  31135  cdlemefr32sn2aw  31138  cdlemefs32sn1aw  31148  cdleme41sn3a  31167  cdleme32fva  31171  cdleme32fva1  31172  cdleme35a  31182  cdleme35b  31184  cdleme35c  31185  cdleme35f  31188  cdleme39a  31199  cdleme42a  31205  cdleme42c  31206  cdleme42b  31212  cdleme42e  31213  cdleme42f  31214  cdleme42g  31215  cdleme42h  31216  cdleme43bN  31224  cdleme46f2g2  31227  cdleme17d2  31229  cdleme17d4  31231  cdleme48fv  31233  cdleme48fvg  31234  cdleme4gfv  31241  cdlemeg46c  31247  cdlemeg46nlpq  31251  cdlemeg46gfre  31266  cdleme48d  31269  cdlemeg49lebilem  31273  cdleme50trn2  31285  cdleme50ltrn  31291  cdleme  31294  cdlemf1  31295  cdlemf  31297  trlord  31303  ltrniotacnvval  31316  ltrniotavalbN  31318  cdlemg1cex  31322  cdlemg2dN  31324  cdlemg2ce  31326  cdlemg2fvlem  31328  cdlemg2idN  31330  cdlemg2kq  31336  cdlemg2l  31337  cdlemg2m  31338  cdlemg4b2  31344  cdlemg7fvN  31358  cdlemg8a  31361  cdlemg10bALTN  31370  cdlemg11aq  31372  cdlemg12d  31380  cdlemg13a  31385  cdlemg13  31386  cdlemg14f  31387  cdlemg14g  31388  cdlemg17a  31395  cdlemg17b  31396  cdlemg27a  31426  cdlemg31b0N  31428  cdlemg31a  31431  cdlemg31b  31432  cdlemg31c  31433  ltrnco  31453  trlcoabs  31455  trlcoabs2N  31456  trlcocnvat  31458  trlconid  31459  trlcolem  31460  trlcone  31462  cdlemg42  31463  cdlemg43  31464  cdlemg46  31469  cdlemg47  31470  tendoeq1  31498  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  cdlemk32  31631  cdlemk28-3  31642  cdlemk19u  31704  cdlemk56w  31707  tendoex  31709  erngdvlem4  31725  erngdvlem4-rN  31733  dia11N  31783  dib11N  31895  cdlemn6  31937  cdlemn7  31938  cdlemn8  31939  cdlemn9  31940  dihordlem6  31948  dihordlem7  31949  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord2pre  31960  dihord2pre2  31961  dihlsscpre  31969  dihvalcq2  31982  dihopelvalcpre  31983  dihord4  31993  dihord6b  31995  dihmeetlem1N  32025  dihglblem3N  32030  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetcN  32037  dihmeetbclemN  32039  dihmeetlem4preN  32041  dihjatc1  32046  dihjatc2N  32047  dihjatc3  32048  dihmeetlem9N  32050  dihmeetlem13N  32054  dihmeetlem20N  32061  dih1dimatlem0  32063  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