MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2l 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  5459  fsnunf  5890  f1oiso2  6031  omeulem2  6785  uniinqs  6943  unxpdomlem3  7274  gruina  8649  addid2  9205  dmdcan  9680  xaddass  10784  xaddass2  10785  xlt2add  10795  xmulasslem3  10821  xadddi2  10832  xadddi2r  10833  expaddzlem  11378  expaddz  11379  expmulz  11381  expdiv  11385  modexp  11469  ccatopth2  11732  o1add  12362  o1mul  12363  o1sub  12364  prmexpb  13072  pcpremul  13172  pcdiv  13181  pcqmul  13182  pcqdiv  13186  4sqlem12  13279  f1ocpbllem  13704  ercpbl  13729  erlecpbl  13730  latjlej12  14451  latmlem12  14467  latj4  14485  latj4rot  14486  mndodcong  15135  cmn4  15386  ablsub4  15392  abladdsub4  15393  lsm4  15430  abvdom  15881  abvres  15882  abvtrivd  15883  lspsnvs  16141  lspsneu  16150  lspfixed  16155  lspexch  16156  lsmcv  16168  lspsolvlem  16169  coe1sclmulfv  16630  cnprest  17307  hausnei2  17371  isreg2  17395  cmpcld  17419  llyrest  17501  nllyrest  17502  elptr  17558  basqtop  17696  hausflimlem  17964  tmdgsum  18078  utop2nei  18233  trcfilu  18277  ssblps  18405  ssbl  18406  prdsxmslem2  18512  tgqioo  18784  metnrm  18845  bndth  18936  cph2ass  19128  lmmbr2  19165  iscau3  19184  bcthlem5  19234  ovolunlem2  19347  dvres2  19752  dvfsumlem2  19864  plyadd  20089  plymul  20090  coeeu  20097  coemullem  20121  aalioulem4  20205  mulcxp  20529  cxplea  20540  cxple2  20541  cxplt2  20542  cxpcn3lem  20584  angcan  20597  ang180lem5  20608  divsqrsumlem  20771  logexprlim  20962  dchrvmasumlema  21147  dchrisum0lema  21161  logdivsum  21180  log2sumbnd  21191  abvcxp  21262  padicabv  21277  1pthon  21544  gxmodid  21820  chscllem4  23095  measxun2  24517  measun  24518  mbfmco2  24568  probun  24630  dedekind  25140  ntrivcvgmul  25183  nofulllem5  25574  brbtwn2  25748  axcontlem4  25810  axcontlem8  25814  cgrcomim  25827  cgrcoml  25834  cgrcomr  25835  cgrdegen  25842  btwnintr  25857  btwnexch3  25858  btwnouttr2  25860  btwnouttr  25862  btwnexch  25863  btwndiff  25865  lineid  25921  idinside  25922  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem12  25936  btwnconn1lem14  25938  btwnconn3  25941  midofsegid  25942  segcon2  25943  brsegle2  25947  btwnoutside  25963  outsideoftr  25967  outsideofeu  25969  linethru  25991  cnres2  26362  heibor  26420  mzpsubst  26695  pellexlem5  26786  pellex  26788  pell14qrexpclnn0  26819  pellfundex  26839  qirropth  26861  monotuz  26894  expmordi  26900  congtr  26920  congmul  26922  congsub  26925  mzpcong  26927  fzmaxdif  26936  jm2.15nn0  26964  symgsssg  27276  symgfisg  27277  idomsubgmo  27382  lsmsat  29491  lkrlsp  29585  lkrlsp2  29586  lkrlsp3  29587  latm4  29716  omlspjN  29744  hlatj4  29856  4noncolr3  29935  4noncolr2  29936  4noncolr1  29937  athgt  29938  3dimlem3a  29942  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  3dim3  29951  1cvratex  29955  hlatexch4  29963  3atlem4  29968  atcvrlln2  30001  atcvrlln  30002  lplnnlelln  30025  lvoli2  30063  lvolnlelln  30066  lvolnlelpln  30067  4atlem11b  30090  4atlem12b  30093  2lplnja  30101  2lplnj  30102  dalemyeo  30114  dath2  30219  lncvrat  30264  cdlemblem  30275  cdlemb  30276  elpaddri  30284  padd4N  30322  llnmod2i2  30345  llnexchb2  30351  dalawlem1  30353  dalawlem2  30354  pclfinN  30382  osumcllem6N  30443  pexmidlem3N  30454  lhp2lt  30483  lhp2at0  30514  lhp2atnle  30515  lhp2atne  30516  lhp2at0nle  30517  lhp2at0ne  30518  lhpelim  30519  lhpmod2i2  30520  lhpmod6i1  30521  lhple  30524  lhpat  30525  lhpat3  30528  ltrncoelN  30625  ltrncoat  30626  ltrncnv  30628  trlat  30651  trl0  30652  ltrnnidn  30656  trlnid  30661  cdlemd7  30686  cdleme0b  30694  cdleme0c  30695  cdleme0fN  30700  cdleme02N  30704  cdleme0ex1N  30705  cdleme0ex2N  30706  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme8  30732  cdleme11a  30742  cdleme17c  30770  cdleme22gb  30776  cdlemeda  30780  cdleme20k  30801  cdleme21a  30807  cdleme21d  30812  cdleme22f2  30829  cdleme22g  30830  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme24  30834  cdleme28  30855  cdlemefrs32fva1  30883  cdlemefr32sn2aw  30886  cdlemefs32sn1aw  30896  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32fva1  30920  cdleme35a  30930  cdleme35b  30932  cdleme35c  30933  cdleme35f  30936  cdleme39a  30947  cdleme42a  30953  cdleme42c  30954  cdleme42b  30960  cdleme42e  30961  cdleme42f  30962  cdleme42g  30963  cdleme42h  30964  cdleme43bN  30972  cdleme46f2g2  30975  cdleme17d2  30977  cdleme17d4  30979  cdleme48fv  30981  cdleme48fvg  30982  cdleme4gfv  30989  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdlemeg46gfre  31014  cdleme48d  31017  cdlemeg49lebilem  31021  cdleme50trn2  31033  cdleme50ltrn  31039  cdleme  31042  cdlemf1  31043  cdlemf  31045  trlord  31051  ltrniotacnvval  31064  ltrniotavalbN  31066  cdlemg1cex  31070  cdlemg2dN  31072  cdlemg2ce  31074  cdlemg2fvlem  31076  cdlemg2idN  31078  cdlemg2kq  31084  cdlemg2l  31085  cdlemg2m  31086  cdlemg4b2  31092  cdlemg7fvN  31106  cdlemg8a  31109  cdlemg10bALTN  31118  cdlemg11aq  31120  cdlemg12d  31128  cdlemg13a  31133  cdlemg13  31134  cdlemg14f  31135  cdlemg14g  31136  cdlemg17a  31143  cdlemg17b  31144  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg31a  31179  cdlemg31b  31180  cdlemg31c  31181  ltrnco  31201  trlcoabs  31203  trlcoabs2N  31204  trlcocnvat  31206  trlconid  31207  trlcolem  31208  trlcone  31210  cdlemg42  31211  cdlemg43  31212  cdlemg46  31217  cdlemg47  31218  tendoeq1  31246  tendoco2  31250  tendoplco2  31261  tendopltp  31262  cdlemh1  31297  cdlemh2  31298  cdlemi1  31300  cdlemi  31302  cdlemk1  31313  cdlemk2  31314  cdlemk3  31315  cdlemk4  31316  cdlemk8  31320  cdlemk9  31321  cdlemk9bN  31322  cdlemk31  31378  cdlemk32  31379  cdlemk28-3  31390  cdlemk19u  31452  cdlemk56w  31455  tendoex  31457  erngdvlem4  31473  erngdvlem4-rN  31481  dia11N  31531  dib11N  31643  cdlemn6  31685  cdlemn7  31686  cdlemn8  31687  cdlemn9  31688  dihordlem6  31696  dihordlem7  31697  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord2pre  31708  dihord2pre2  31709  dihlsscpre  31717  dihvalcq2  31730  dihopelvalcpre  31731  dihord4  31741  dihord6b  31743  dihmeetlem1N  31773  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbclemN  31787  dihmeetlem4preN  31789  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  dihmeetlem9N  31798  dihmeetlem13N  31802  dihmeetlem20N  31809  dih1dimatlem0  31811  mapdpglem24  32187  mapdpglem32  32188  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  mapdh9aOLDN  32274  hdmap14lem6  32359
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