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

Theorem simp2l 1031
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 458 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1027 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl2l  1058  simpr2l  1064  simp12l  1118  simp22l  1124  simp32l  1130  funprg  5650  fsnunf  6117  f1oiso2  6258  omeulem2  7292  uniinqs  7451  unxpdomlem3  7784  gruina  9242  dedekind  9796  addid2  9815  dmdcan  10316  xaddass  11535  xaddass2  11536  xlt2add  11546  xmulasslem3  11572  xadddi2  11583  xadddi2r  11584  expaddzlem  12312  expaddz  12313  expmulz  12315  expdiv  12320  modexp  12404  ccatopth2  12812  swrdco  12919  o1add  13655  o1mul  13656  o1sub  13657  ntrivcvgmul  13936  prmexpb  14641  pcpremul  14756  pcdiv  14765  pcqmul  14766  pcqdiv  14770  4sqlem12  14863  f1ocpbllem  15381  ercpbl  15406  erlecpbl  15407  latjlej12  16264  latmlem12  16280  latj4  16298  latj4rot  16299  symgsssg  17059  symgfisg  17060  mndodcong  17133  cmn4  17384  ablsub4  17390  abladdsub4  17391  lsm4  17433  abvdom  18001  abvres  18002  abvtrivd  18003  lspsnvs  18272  lspsneu  18281  lspfixed  18286  lspexch  18287  lsmcv  18299  lspsolvlem  18300  coe1sclmulfv  18811  matvscacell  19392  m1detdiag  19553  cramerimplem3  19641  cnprest  20236  hausnei2  20300  isreg2  20324  cmpcld  20348  llyrest  20431  nllyrest  20432  elptr  20519  basqtop  20657  hausflimlem  20925  tmdgsum  21041  utop2nei  21196  trcfilu  21240  ssblps  21368  ssbl  21369  prdsxmslem2  21475  tgqioo  21729  metnrm  21790  bndth  21882  cph2ass  22083  lmmbr2  22122  iscau3  22141  bcthlem5  22189  ovolunlem2  22329  dvres2  22744  dvfsumlem2  22856  plyadd  23039  plymul  23040  coeeu  23047  coemullem  23072  aalioulem4  23156  mulcxp  23495  cxplea  23506  cxple2  23507  cxplt2  23508  cxpcn3lem  23552  angcan  23596  ang180lem5  23607  divsqrtsumlem  23770  logexprlim  24016  dchrvmasumlema  24201  dchrisum0lema  24215  logdivsum  24234  log2sumbnd  24245  abvcxp  24316  padicabv  24331  tghilberti2  24542  brbtwn2  24781  axcontlem4  24843  axcontlem8  24847  1pthon  25166  clwwlkel  25366  gxmodid  25852  chscllem4  27128  orngmul  28405  measxun2  28871  measun  28872  mbfmco2  28926  probun  29078  nofulllem5  30380  cgrcomim  30541  cgrcoml  30548  cgrcomr  30549  cgrdegen  30556  btwnintr  30571  btwnexch3  30572  btwnouttr2  30574  btwnouttr  30576  btwnexch  30577  btwndiff  30579  lineid  30635  idinside  30636  btwnconn1lem7  30645  btwnconn1lem8  30646  btwnconn1lem9  30647  btwnconn1lem12  30650  btwnconn1lem14  30652  btwnconn3  30655  midofsegid  30656  segcon2  30657  brsegle2  30661  btwnoutside  30677  outsideoftr  30681  outsideofeu  30683  linethru  30705  cnres2  31798  heibor  31856  lsmsat  32282  lkrlsp  32376  lkrlsp2  32377  lkrlsp3  32378  latm4  32507  omlspjN  32535  hlatj4  32647  4noncolr3  32726  4noncolr2  32727  4noncolr1  32728  athgt  32729  3dimlem3a  32733  3dimlem4a  32736  3dimlem4  32737  3dimlem4OLDN  32738  3dim3  32742  1cvratex  32746  hlatexch4  32754  3atlem4  32759  atcvrlln2  32792  atcvrlln  32793  lplnnlelln  32816  lvoli2  32854  lvolnlelln  32857  lvolnlelpln  32858  4atlem11b  32881  4atlem12b  32884  2lplnja  32892  2lplnj  32893  dalemyeo  32905  dath2  33010  lncvrat  33055  cdlemblem  33066  cdlemb  33067  elpaddri  33075  padd4N  33113  llnmod2i2  33136  llnexchb2  33142  dalawlem1  33144  dalawlem2  33145  pclfinN  33173  osumcllem6N  33234  pexmidlem3N  33245  lhp2lt  33274  lhp2at0  33305  lhp2atnle  33306  lhp2atne  33307  lhp2at0nle  33308  lhp2at0ne  33309  lhpelim  33310  lhpmod2i2  33311  lhpmod6i1  33312  lhple  33315  lhpat  33316  lhpat3  33319  ltrncoelN  33416  ltrncoat  33417  ltrncnv  33419  trlat  33443  trl0  33444  ltrnnidn  33448  trlnid  33453  cdlemd7  33478  cdleme0b  33486  cdleme0c  33487  cdleme0fN  33492  cdleme02N  33496  cdleme0ex1N  33497  cdleme0ex2N  33498  cdleme7aa  33516  cdleme7c  33519  cdleme7d  33520  cdleme7e  33521  cdleme7ga  33522  cdleme7  33523  cdleme8  33524  cdleme11a  33534  cdleme17c  33562  cdleme22gb  33568  cdlemeda  33572  cdleme20k  33594  cdleme21a  33600  cdleme21d  33605  cdleme22f2  33622  cdleme22g  33623  cdleme23a  33624  cdleme23b  33625  cdleme23c  33626  cdleme24  33627  cdleme28  33648  cdlemefrs32fva1  33676  cdlemefr32sn2aw  33679  cdlemefs32sn1aw  33689  cdleme41sn3a  33708  cdleme32fva  33712  cdleme32fva1  33713  cdleme35a  33723  cdleme35b  33725  cdleme35c  33726  cdleme35f  33729  cdleme39a  33740  cdleme42a  33746  cdleme42c  33747  cdleme42b  33753  cdleme42e  33754  cdleme42f  33755  cdleme42g  33756  cdleme42h  33757  cdleme43bN  33765  cdleme46f2g2  33768  cdleme17d2  33770  cdleme17d4  33772  cdleme48fv  33774  cdleme48fvg  33775  cdleme4gfv  33782  cdlemeg46c  33788  cdlemeg46nlpq  33792  cdlemeg46gfre  33807  cdleme48d  33810  cdlemeg49lebilem  33814  cdleme50trn2  33826  cdleme50ltrn  33832  cdleme  33835  cdlemf1  33836  cdlemf  33838  trlord  33844  ltrniotacnvval  33857  ltrniotavalbN  33859  cdlemg1cex  33863  cdlemg2dN  33865  cdlemg2ce  33867  cdlemg2fvlem  33869  cdlemg2idN  33871  cdlemg2kq  33877  cdlemg2l  33878  cdlemg2m  33879  cdlemg4b2  33885  cdlemg7fvN  33899  cdlemg8a  33902  cdlemg10bALTN  33911  cdlemg11aq  33913  cdlemg12d  33921  cdlemg13a  33926  cdlemg13  33927  cdlemg14f  33928  cdlemg14g  33929  cdlemg17a  33936  cdlemg17b  33937  cdlemg27a  33967  cdlemg31b0N  33969  cdlemg31a  33972  cdlemg31b  33973  cdlemg31c  33974  ltrnco  33994  trlcoabs  33996  trlcoabs2N  33997  trlcocnvat  33999  trlconid  34000  trlcolem  34001  trlcone  34003  cdlemg42  34004  cdlemg43  34005  cdlemg46  34010  cdlemg47  34011  tendoeq1  34039  tendoco2  34043  tendoplco2  34054  tendopltp  34055  cdlemh1  34090  cdlemh2  34091  cdlemi1  34093  cdlemi  34095  cdlemk1  34106  cdlemk2  34107  cdlemk3  34108  cdlemk4  34109  cdlemk8  34113  cdlemk9  34114  cdlemk9bN  34115  cdlemk31  34171  cdlemk32  34172  cdlemk28-3  34183  cdlemk19u  34245  cdlemk56w  34248  tendoex  34250  erngdvlem4  34266  erngdvlem4-rN  34274  dia11N  34324  dib11N  34436  cdlemn6  34478  cdlemn7  34479  cdlemn8  34480  cdlemn9  34481  dihordlem6  34489  dihordlem7  34490  dihord1  34494  dihord2a  34495  dihord2b  34496  dihord2pre  34501  dihord2pre2  34502  dihlsscpre  34510  dihvalcq2  34523  dihopelvalcpre  34524  dihord4  34534  dihord6b  34536  dihmeetlem1N  34566  dihglblem3N  34571  dihmeetlem2N  34575  dihglbcpreN  34576  dihmeetcN  34578  dihmeetbclemN  34580  dihmeetlem4preN  34582  dihjatc1  34587  dihjatc2N  34588  dihjatc3  34589  dihmeetlem9N  34591  dihmeetlem13N  34595  dihmeetlem20N  34602  dih1dimatlem0  34604  mapdpglem24  34980  mapdpglem32  34981  baerlem3lem2  34986  baerlem5alem2  34987  baerlem5blem2  34988  mapdh9aOLDN  35067  hdmap14lem6  35152  mzpsubst  35298  pellexlem5  35386  pellex  35388  pell14qrexpclnn0  35419  pellfundex  35439  qirropth  35461  monotuz  35494  expmordi  35500  congtr  35520  congmul  35522  congsub  35525  mzpcong  35527  fzmaxdif  35536  jm2.15nn0  35563  idomsubgmo  35770  iunrelexpmin1  35938  iunrelexpmin2  35942  trclimalb2  35956  fourierdlem42  37579  fourierdlem48  37585  fourierdlem80  37617  lidldomn1  38678  rngccatidALTV  38748  coe1sclmulval  38936  lincdifsn  38976
  Copyright terms: Public domain W3C validator