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

Theorem simp2l 1020
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 455 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1016 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simpl2l  1047  simpr2l  1053  simp12l  1107  simp22l  1113  simp32l  1119  funprg  5545  fsnunf  6011  f1oiso2  6149  omeulem2  7150  uniinqs  7309  unxpdomlem3  7642  gruina  9107  dedekind  9655  addid2  9674  dmdcan  10171  xaddass  11362  xaddass2  11363  xlt2add  11373  xmulasslem3  11399  xadddi2  11410  xadddi2r  11411  expaddzlem  12112  expaddz  12113  expmulz  12115  expdiv  12119  modexp  12203  ccatopth2  12607  swrdco  12714  o1add  13438  o1mul  13439  o1sub  13440  ntrivcvgmul  13713  prmexpb  14260  pcpremul  14369  pcdiv  14378  pcqmul  14379  pcqdiv  14383  4sqlem12  14476  f1ocpbllem  14931  ercpbl  14956  erlecpbl  14957  latjlej12  15814  latmlem12  15830  latj4  15848  latj4rot  15849  symgsssg  16609  symgfisg  16610  mndodcong  16683  cmn4  16934  ablsub4  16940  abladdsub4  16941  lsm4  16983  abvdom  17600  abvres  17601  abvtrivd  17602  lspsnvs  17873  lspsneu  17882  lspfixed  17887  lspexch  17888  lsmcv  17900  lspsolvlem  17901  coe1sclmulfv  18437  matvscacell  19023  m1detdiag  19184  cramerimplem3  19272  cnprest  19876  hausnei2  19940  isreg2  19964  cmpcld  19988  llyrest  20071  nllyrest  20072  elptr  20159  basqtop  20297  hausflimlem  20565  tmdgsum  20679  utop2nei  20838  trcfilu  20882  ssblps  21010  ssbl  21011  prdsxmslem2  21117  tgqioo  21390  metnrm  21451  bndth  21543  cph2ass  21744  lmmbr2  21783  iscau3  21802  bcthlem5  21852  ovolunlem2  21994  dvres2  22401  dvfsumlem2  22513  plyadd  22699  plymul  22700  coeeu  22707  coemullem  22732  aalioulem4  22816  mulcxp  23153  cxplea  23164  cxple2  23165  cxplt2  23166  cxpcn3lem  23208  angcan  23252  ang180lem5  23263  divsqrtsumlem  23426  logexprlim  23617  dchrvmasumlema  23802  dchrisum0lema  23816  logdivsum  23835  log2sumbnd  23846  abvcxp  23917  padicabv  23932  tghilberti2  24138  brbtwn2  24329  axcontlem4  24391  axcontlem8  24395  1pthon  24714  clwwlkel  24914  gxmodid  25398  chscllem4  26675  orngmul  27947  measxun2  28337  measun  28338  mbfmco2  28392  probun  28541  nofulllem5  29631  cgrcomim  29792  cgrcoml  29799  cgrcomr  29800  cgrdegen  29807  btwnintr  29822  btwnexch3  29823  btwnouttr2  29825  btwnouttr  29827  btwnexch  29828  btwndiff  29830  lineid  29886  idinside  29887  btwnconn1lem7  29896  btwnconn1lem8  29897  btwnconn1lem9  29898  btwnconn1lem12  29901  btwnconn1lem14  29903  btwnconn3  29906  midofsegid  29907  segcon2  29908  brsegle2  29912  btwnoutside  29928  outsideoftr  29932  outsideofeu  29934  linethru  29956  cnres2  30425  heibor  30483  mzpsubst  30846  pellexlem5  30934  pellex  30936  pell14qrexpclnn0  30967  pellfundex  30987  qirropth  31009  monotuz  31042  expmordi  31048  congtr  31068  congmul  31070  congsub  31073  mzpcong  31075  fzmaxdif  31084  jm2.15nn0  31111  idomsubgmo  31323  fourierdlem42  32097  fourierdlem48  32103  fourierdlem80  32135  lidldomn1  32927  rngccatidALTV  32997  coe1sclmulval  33185  lincdifsn  33225  lsmsat  35146  lkrlsp  35240  lkrlsp2  35241  lkrlsp3  35242  latm4  35371  omlspjN  35399  hlatj4  35511  4noncolr3  35590  4noncolr2  35591  4noncolr1  35592  athgt  35593  3dimlem3a  35597  3dimlem4a  35600  3dimlem4  35601  3dimlem4OLDN  35602  3dim3  35606  1cvratex  35610  hlatexch4  35618  3atlem4  35623  atcvrlln2  35656  atcvrlln  35657  lplnnlelln  35680  lvoli2  35718  lvolnlelln  35721  lvolnlelpln  35722  4atlem11b  35745  4atlem12b  35748  2lplnja  35756  2lplnj  35757  dalemyeo  35769  dath2  35874  lncvrat  35919  cdlemblem  35930  cdlemb  35931  elpaddri  35939  padd4N  35977  llnmod2i2  36000  llnexchb2  36006  dalawlem1  36008  dalawlem2  36009  pclfinN  36037  osumcllem6N  36098  pexmidlem3N  36109  lhp2lt  36138  lhp2at0  36169  lhp2atnle  36170  lhp2atne  36171  lhp2at0nle  36172  lhp2at0ne  36173  lhpelim  36174  lhpmod2i2  36175  lhpmod6i1  36176  lhple  36179  lhpat  36180  lhpat3  36183  ltrncoelN  36280  ltrncoat  36281  ltrncnv  36283  trlat  36307  trl0  36308  ltrnnidn  36312  trlnid  36317  cdlemd7  36342  cdleme0b  36350  cdleme0c  36351  cdleme0fN  36356  cdleme02N  36360  cdleme0ex1N  36361  cdleme0ex2N  36362  cdleme7aa  36380  cdleme7c  36383  cdleme7d  36384  cdleme7e  36385  cdleme7ga  36386  cdleme7  36387  cdleme8  36388  cdleme11a  36398  cdleme17c  36426  cdleme22gb  36432  cdlemeda  36436  cdleme20k  36458  cdleme21a  36464  cdleme21d  36469  cdleme22f2  36486  cdleme22g  36487  cdleme23a  36488  cdleme23b  36489  cdleme23c  36490  cdleme24  36491  cdleme28  36512  cdlemefrs32fva1  36540  cdlemefr32sn2aw  36543  cdlemefs32sn1aw  36553  cdleme41sn3a  36572  cdleme32fva  36576  cdleme32fva1  36577  cdleme35a  36587  cdleme35b  36589  cdleme35c  36590  cdleme35f  36593  cdleme39a  36604  cdleme42a  36610  cdleme42c  36611  cdleme42b  36617  cdleme42e  36618  cdleme42f  36619  cdleme42g  36620  cdleme42h  36621  cdleme43bN  36629  cdleme46f2g2  36632  cdleme17d2  36634  cdleme17d4  36636  cdleme48fv  36638  cdleme48fvg  36639  cdleme4gfv  36646  cdlemeg46c  36652  cdlemeg46nlpq  36656  cdlemeg46gfre  36671  cdleme48d  36674  cdlemeg49lebilem  36678  cdleme50trn2  36690  cdleme50ltrn  36696  cdleme  36699  cdlemf1  36700  cdlemf  36702  trlord  36708  ltrniotacnvval  36721  ltrniotavalbN  36723  cdlemg1cex  36727  cdlemg2dN  36729  cdlemg2ce  36731  cdlemg2fvlem  36733  cdlemg2idN  36735  cdlemg2kq  36741  cdlemg2l  36742  cdlemg2m  36743  cdlemg4b2  36749  cdlemg7fvN  36763  cdlemg8a  36766  cdlemg10bALTN  36775  cdlemg11aq  36777  cdlemg12d  36785  cdlemg13a  36790  cdlemg13  36791  cdlemg14f  36792  cdlemg14g  36793  cdlemg17a  36800  cdlemg17b  36801  cdlemg27a  36831  cdlemg31b0N  36833  cdlemg31a  36836  cdlemg31b  36837  cdlemg31c  36838  ltrnco  36858  trlcoabs  36860  trlcoabs2N  36861  trlcocnvat  36863  trlconid  36864  trlcolem  36865  trlcone  36867  cdlemg42  36868  cdlemg43  36869  cdlemg46  36874  cdlemg47  36875  tendoeq1  36903  tendoco2  36907  tendoplco2  36918  tendopltp  36919  cdlemh1  36954  cdlemh2  36955  cdlemi1  36957  cdlemi  36959  cdlemk1  36970  cdlemk2  36971  cdlemk3  36972  cdlemk4  36973  cdlemk8  36977  cdlemk9  36978  cdlemk9bN  36979  cdlemk31  37035  cdlemk32  37036  cdlemk28-3  37047  cdlemk19u  37109  cdlemk56w  37112  tendoex  37114  erngdvlem4  37130  erngdvlem4-rN  37138  dia11N  37188  dib11N  37300  cdlemn6  37342  cdlemn7  37343  cdlemn8  37344  cdlemn9  37345  dihordlem6  37353  dihordlem7  37354  dihord1  37358  dihord2a  37359  dihord2b  37360  dihord2pre  37365  dihord2pre2  37366  dihlsscpre  37374  dihvalcq2  37387  dihopelvalcpre  37388  dihord4  37398  dihord6b  37400  dihmeetlem1N  37430  dihglblem3N  37435  dihmeetlem2N  37439  dihglbcpreN  37440  dihmeetcN  37442  dihmeetbclemN  37444  dihmeetlem4preN  37446  dihjatc1  37451  dihjatc2N  37452  dihjatc3  37453  dihmeetlem9N  37455  dihmeetlem13N  37459  dihmeetlem20N  37466  dih1dimatlem0  37468  mapdpglem24  37844  mapdpglem32  37845  baerlem3lem2  37850  baerlem5alem2  37851  baerlem5blem2  37852  mapdh9aOLDN  37931  hdmap14lem6  38016  iunrelexpmin1  38225  iunrelexpmin2  38226  trclimalb2  38257
  Copyright terms: Public domain W3C validator