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

Theorem simp2l 1017
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 457 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1013 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 185  df-an 371  df-3an 970
This theorem is referenced by:  simpl2l  1044  simpr2l  1050  simp12l  1104  simp22l  1110  simp32l  1116  funprg  5628  fsnunf  6090  f1oiso2  6227  omeulem2  7222  uniinqs  7381  unxpdomlem3  7716  gruina  9185  dedekind  9732  addid2  9751  dmdcan  10243  xaddass  11430  xaddass2  11431  xlt2add  11441  xmulasslem3  11467  xadddi2  11478  xadddi2r  11479  expaddzlem  12164  expaddz  12165  expmulz  12167  expdiv  12171  modexp  12256  ccatopth2  12646  swrdco  12753  o1add  13385  o1mul  13386  o1sub  13387  prmexpb  14106  pcpremul  14215  pcdiv  14224  pcqmul  14225  pcqdiv  14229  4sqlem12  14322  f1ocpbllem  14768  ercpbl  14793  erlecpbl  14794  latjlej12  15543  latmlem12  15559  latj4  15577  latj4rot  15578  symgsssg  16281  symgfisg  16282  mndodcong  16355  cmn4  16606  ablsub4  16612  abladdsub4  16613  lsm4  16652  abvdom  17263  abvres  17264  abvtrivd  17265  lspsnvs  17536  lspsneu  17545  lspfixed  17550  lspexch  17551  lsmcv  17563  lspsolvlem  17564  coe1sclmulfv  18088  m1detdiag  18859  cramerimplem3  18947  cnprest  19549  hausnei2  19613  isreg2  19637  cmpcld  19661  llyrest  19745  nllyrest  19746  elptr  19802  basqtop  19940  hausflimlem  20208  tmdgsum  20322  utop2nei  20481  trcfilu  20525  ssblps  20653  ssbl  20654  prdsxmslem2  20760  tgqioo  21033  metnrm  21094  bndth  21186  cph2ass  21387  lmmbr2  21426  iscau3  21445  bcthlem5  21495  ovolunlem2  21637  dvres2  22044  dvfsumlem2  22156  plyadd  22342  plymul  22343  coeeu  22350  coemullem  22374  aalioulem4  22458  mulcxp  22787  cxplea  22798  cxple2  22799  cxplt2  22800  cxpcn3lem  22842  angcan  22855  ang180lem5  22866  divsqrsumlem  23030  logexprlim  23221  dchrvmasumlema  23406  dchrisum0lema  23420  logdivsum  23439  log2sumbnd  23450  abvcxp  23521  padicabv  23536  tghilbert1_2  23725  brbtwn2  23877  axcontlem4  23939  axcontlem8  23943  1pthon  24255  clwwlkel  24455  gxmodid  24943  chscllem4  26220  orngmul  27442  measxun2  27807  measun  27808  mbfmco2  27862  probun  27984  ntrivcvgmul  28599  nofulllem5  29029  cgrcomim  29202  cgrcoml  29209  cgrcomr  29210  cgrdegen  29217  btwnintr  29232  btwnexch3  29233  btwnouttr2  29235  btwnouttr  29237  btwnexch  29238  btwndiff  29240  lineid  29296  idinside  29297  btwnconn1lem7  29306  btwnconn1lem8  29307  btwnconn1lem9  29308  btwnconn1lem12  29311  btwnconn1lem14  29313  btwnconn3  29316  midofsegid  29317  segcon2  29318  brsegle2  29322  btwnoutside  29338  outsideoftr  29342  outsideofeu  29344  linethru  29366  cnres2  29849  heibor  29907  mzpsubst  30272  pellexlem5  30360  pellex  30362  pell14qrexpclnn0  30393  pellfundex  30413  qirropth  30435  monotuz  30468  expmordi  30474  congtr  30494  congmul  30496  congsub  30499  mzpcong  30501  fzmaxdif  30510  jm2.15nn0  30538  idomsubgmo  30749  mullimc  31113  mullimcf  31120  fourierdlem42  31404  fourierdlem48  31410  fourierdlem80  31442  coe1sclmulval  31933  lincdifsn  31973  lsmsat  33680  lkrlsp  33774  lkrlsp2  33775  lkrlsp3  33776  latm4  33905  omlspjN  33933  hlatj4  34045  4noncolr3  34124  4noncolr2  34125  4noncolr1  34126  athgt  34127  3dimlem3a  34131  3dimlem4a  34134  3dimlem4  34135  3dimlem4OLDN  34136  3dim3  34140  1cvratex  34144  hlatexch4  34152  3atlem4  34157  atcvrlln2  34190  atcvrlln  34191  lplnnlelln  34214  lvoli2  34252  lvolnlelln  34255  lvolnlelpln  34256  4atlem11b  34279  4atlem12b  34282  2lplnja  34290  2lplnj  34291  dalemyeo  34303  dath2  34408  lncvrat  34453  cdlemblem  34464  cdlemb  34465  elpaddri  34473  padd4N  34511  llnmod2i2  34534  llnexchb2  34540  dalawlem1  34542  dalawlem2  34543  pclfinN  34571  osumcllem6N  34632  pexmidlem3N  34643  lhp2lt  34672  lhp2at0  34703  lhp2atnle  34704  lhp2atne  34705  lhp2at0nle  34706  lhp2at0ne  34707  lhpelim  34708  lhpmod2i2  34709  lhpmod6i1  34710  lhple  34713  lhpat  34714  lhpat3  34717  ltrncoelN  34814  ltrncoat  34815  ltrncnv  34817  trlat  34840  trl0  34841  ltrnnidn  34845  trlnid  34850  cdlemd7  34875  cdleme0b  34883  cdleme0c  34884  cdleme0fN  34889  cdleme02N  34893  cdleme0ex1N  34894  cdleme0ex2N  34895  cdleme7aa  34913  cdleme7c  34916  cdleme7d  34917  cdleme7e  34918  cdleme7ga  34919  cdleme7  34920  cdleme8  34921  cdleme11a  34931  cdleme17c  34959  cdleme22gb  34965  cdlemeda  34969  cdleme20k  34990  cdleme21a  34996  cdleme21d  35001  cdleme22f2  35018  cdleme22g  35019  cdleme23a  35020  cdleme23b  35021  cdleme23c  35022  cdleme24  35023  cdleme28  35044  cdlemefrs32fva1  35072  cdlemefr32sn2aw  35075  cdlemefs32sn1aw  35085  cdleme41sn3a  35104  cdleme32fva  35108  cdleme32fva1  35109  cdleme35a  35119  cdleme35b  35121  cdleme35c  35122  cdleme35f  35125  cdleme39a  35136  cdleme42a  35142  cdleme42c  35143  cdleme42b  35149  cdleme42e  35150  cdleme42f  35151  cdleme42g  35152  cdleme42h  35153  cdleme43bN  35161  cdleme46f2g2  35164  cdleme17d2  35166  cdleme17d4  35168  cdleme48fv  35170  cdleme48fvg  35171  cdleme4gfv  35178  cdlemeg46c  35184  cdlemeg46nlpq  35188  cdlemeg46gfre  35203  cdleme48d  35206  cdlemeg49lebilem  35210  cdleme50trn2  35222  cdleme50ltrn  35228  cdleme  35231  cdlemf1  35232  cdlemf  35234  trlord  35240  ltrniotacnvval  35253  ltrniotavalbN  35255  cdlemg1cex  35259  cdlemg2dN  35261  cdlemg2ce  35263  cdlemg2fvlem  35265  cdlemg2idN  35267  cdlemg2kq  35273  cdlemg2l  35274  cdlemg2m  35275  cdlemg4b2  35281  cdlemg7fvN  35295  cdlemg8a  35298  cdlemg10bALTN  35307  cdlemg11aq  35309  cdlemg12d  35317  cdlemg13a  35322  cdlemg13  35323  cdlemg14f  35324  cdlemg14g  35325  cdlemg17a  35332  cdlemg17b  35333  cdlemg27a  35363  cdlemg31b0N  35365  cdlemg31a  35368  cdlemg31b  35369  cdlemg31c  35370  ltrnco  35390  trlcoabs  35392  trlcoabs2N  35393  trlcocnvat  35395  trlconid  35396  trlcolem  35397  trlcone  35399  cdlemg42  35400  cdlemg43  35401  cdlemg46  35406  cdlemg47  35407  tendoeq1  35435  tendoco2  35439  tendoplco2  35450  tendopltp  35451  cdlemh1  35486  cdlemh2  35487  cdlemi1  35489  cdlemi  35491  cdlemk1  35502  cdlemk2  35503  cdlemk3  35504  cdlemk4  35505  cdlemk8  35509  cdlemk9  35510  cdlemk9bN  35511  cdlemk31  35567  cdlemk32  35568  cdlemk28-3  35579  cdlemk19u  35641  cdlemk56w  35644  tendoex  35646  erngdvlem4  35662  erngdvlem4-rN  35670  dia11N  35720  dib11N  35832  cdlemn6  35874  cdlemn7  35875  cdlemn8  35876  cdlemn9  35877  dihordlem6  35885  dihordlem7  35886  dihord1  35890  dihord2a  35891  dihord2b  35892  dihord2pre  35897  dihord2pre2  35898  dihlsscpre  35906  dihvalcq2  35919  dihopelvalcpre  35920  dihord4  35930  dihord6b  35932  dihmeetlem1N  35962  dihglblem3N  35967  dihmeetlem2N  35971  dihglbcpreN  35972  dihmeetcN  35974  dihmeetbclemN  35976  dihmeetlem4preN  35978  dihjatc1  35983  dihjatc2N  35984  dihjatc3  35985  dihmeetlem9N  35987  dihmeetlem13N  35991  dihmeetlem20N  35998  dih1dimatlem0  36000  mapdpglem24  36376  mapdpglem32  36377  baerlem3lem2  36382  baerlem5alem2  36383  baerlem5blem2  36384  mapdh9aOLDN  36463  hdmap14lem6  36548
  Copyright terms: Public domain W3C validator