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

Theorem simp2l 1023
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 1019 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  simpl2l  1050  simpr2l  1056  simp12l  1110  simp22l  1116  simp32l  1122  funprg  5627  fsnunf  6094  f1oiso2  6233  omeulem2  7234  uniinqs  7393  unxpdomlem3  7728  gruina  9199  dedekind  9747  addid2  9766  dmdcan  10260  xaddass  11450  xaddass2  11451  xlt2add  11461  xmulasslem3  11487  xadddi2  11498  xadddi2r  11499  expaddzlem  12188  expaddz  12189  expmulz  12191  expdiv  12195  modexp  12280  ccatopth2  12675  swrdco  12782  o1add  13415  o1mul  13416  o1sub  13417  prmexpb  14135  pcpremul  14244  pcdiv  14253  pcqmul  14254  pcqdiv  14258  4sqlem12  14351  f1ocpbllem  14798  ercpbl  14823  erlecpbl  14824  latjlej12  15571  latmlem12  15587  latj4  15605  latj4rot  15606  symgsssg  16366  symgfisg  16367  mndodcong  16440  cmn4  16691  ablsub4  16697  abladdsub4  16698  lsm4  16740  abvdom  17361  abvres  17362  abvtrivd  17363  lspsnvs  17634  lspsneu  17643  lspfixed  17648  lspexch  17649  lsmcv  17661  lspsolvlem  17662  coe1sclmulfv  18198  matvscacell  18811  m1detdiag  18972  cramerimplem3  19060  cnprest  19663  hausnei2  19727  isreg2  19751  cmpcld  19775  llyrest  19859  nllyrest  19860  elptr  19947  basqtop  20085  hausflimlem  20353  tmdgsum  20467  utop2nei  20626  trcfilu  20670  ssblps  20798  ssbl  20799  prdsxmslem2  20905  tgqioo  21178  metnrm  21239  bndth  21331  cph2ass  21532  lmmbr2  21571  iscau3  21590  bcthlem5  21640  ovolunlem2  21782  dvres2  22189  dvfsumlem2  22301  plyadd  22487  plymul  22488  coeeu  22495  coemullem  22519  aalioulem4  22603  mulcxp  22938  cxplea  22949  cxple2  22950  cxplt2  22951  cxpcn3lem  22993  angcan  23006  ang180lem5  23017  divsqrtsumlem  23181  logexprlim  23372  dchrvmasumlema  23557  dchrisum0lema  23571  logdivsum  23590  log2sumbnd  23601  abvcxp  23672  padicabv  23687  tghilbert1_2  23890  brbtwn2  24080  axcontlem4  24142  axcontlem8  24146  1pthon  24465  clwwlkel  24665  gxmodid  25153  chscllem4  26430  orngmul  27666  measxun2  28054  measun  28055  mbfmco2  28109  probun  28231  ntrivcvgmul  29011  nofulllem5  29441  cgrcomim  29614  cgrcoml  29621  cgrcomr  29622  cgrdegen  29629  btwnintr  29644  btwnexch3  29645  btwnouttr2  29647  btwnouttr  29649  btwnexch  29650  btwndiff  29652  lineid  29708  idinside  29709  btwnconn1lem7  29718  btwnconn1lem8  29719  btwnconn1lem9  29720  btwnconn1lem12  29723  btwnconn1lem14  29725  btwnconn3  29728  midofsegid  29729  segcon2  29730  brsegle2  29734  btwnoutside  29750  outsideoftr  29754  outsideofeu  29756  linethru  29778  cnres2  30234  heibor  30292  mzpsubst  30656  pellexlem5  30744  pellex  30746  pell14qrexpclnn0  30777  pellfundex  30797  qirropth  30819  monotuz  30852  expmordi  30858  congtr  30878  congmul  30880  congsub  30883  mzpcong  30885  fzmaxdif  30894  jm2.15nn0  30920  idomsubgmo  31131  fourierdlem42  31820  fourierdlem48  31826  fourierdlem80  31858  lidldomn1  32434  rngccatidOLD  32534  coe1sclmulval  32715  lincdifsn  32755  lsmsat  34467  lkrlsp  34561  lkrlsp2  34562  lkrlsp3  34563  latm4  34692  omlspjN  34720  hlatj4  34832  4noncolr3  34911  4noncolr2  34912  4noncolr1  34913  athgt  34914  3dimlem3a  34918  3dimlem4a  34921  3dimlem4  34922  3dimlem4OLDN  34923  3dim3  34927  1cvratex  34931  hlatexch4  34939  3atlem4  34944  atcvrlln2  34977  atcvrlln  34978  lplnnlelln  35001  lvoli2  35039  lvolnlelln  35042  lvolnlelpln  35043  4atlem11b  35066  4atlem12b  35069  2lplnja  35077  2lplnj  35078  dalemyeo  35090  dath2  35195  lncvrat  35240  cdlemblem  35251  cdlemb  35252  elpaddri  35260  padd4N  35298  llnmod2i2  35321  llnexchb2  35327  dalawlem1  35329  dalawlem2  35330  pclfinN  35358  osumcllem6N  35419  pexmidlem3N  35430  lhp2lt  35459  lhp2at0  35490  lhp2atnle  35491  lhp2atne  35492  lhp2at0nle  35493  lhp2at0ne  35494  lhpelim  35495  lhpmod2i2  35496  lhpmod6i1  35497  lhple  35500  lhpat  35501  lhpat3  35504  ltrncoelN  35601  ltrncoat  35602  ltrncnv  35604  trlat  35628  trl0  35629  ltrnnidn  35633  trlnid  35638  cdlemd7  35663  cdleme0b  35671  cdleme0c  35672  cdleme0fN  35677  cdleme02N  35681  cdleme0ex1N  35682  cdleme0ex2N  35683  cdleme7aa  35701  cdleme7c  35704  cdleme7d  35705  cdleme7e  35706  cdleme7ga  35707  cdleme7  35708  cdleme8  35709  cdleme11a  35719  cdleme17c  35747  cdleme22gb  35753  cdlemeda  35757  cdleme20k  35779  cdleme21a  35785  cdleme21d  35790  cdleme22f2  35807  cdleme22g  35808  cdleme23a  35809  cdleme23b  35810  cdleme23c  35811  cdleme24  35812  cdleme28  35833  cdlemefrs32fva1  35861  cdlemefr32sn2aw  35864  cdlemefs32sn1aw  35874  cdleme41sn3a  35893  cdleme32fva  35897  cdleme32fva1  35898  cdleme35a  35908  cdleme35b  35910  cdleme35c  35911  cdleme35f  35914  cdleme39a  35925  cdleme42a  35931  cdleme42c  35932  cdleme42b  35938  cdleme42e  35939  cdleme42f  35940  cdleme42g  35941  cdleme42h  35942  cdleme43bN  35950  cdleme46f2g2  35953  cdleme17d2  35955  cdleme17d4  35957  cdleme48fv  35959  cdleme48fvg  35960  cdleme4gfv  35967  cdlemeg46c  35973  cdlemeg46nlpq  35977  cdlemeg46gfre  35992  cdleme48d  35995  cdlemeg49lebilem  35999  cdleme50trn2  36011  cdleme50ltrn  36017  cdleme  36020  cdlemf1  36021  cdlemf  36023  trlord  36029  ltrniotacnvval  36042  ltrniotavalbN  36044  cdlemg1cex  36048  cdlemg2dN  36050  cdlemg2ce  36052  cdlemg2fvlem  36054  cdlemg2idN  36056  cdlemg2kq  36062  cdlemg2l  36063  cdlemg2m  36064  cdlemg4b2  36070  cdlemg7fvN  36084  cdlemg8a  36087  cdlemg10bALTN  36096  cdlemg11aq  36098  cdlemg12d  36106  cdlemg13a  36111  cdlemg13  36112  cdlemg14f  36113  cdlemg14g  36114  cdlemg17a  36121  cdlemg17b  36122  cdlemg27a  36152  cdlemg31b0N  36154  cdlemg31a  36157  cdlemg31b  36158  cdlemg31c  36159  ltrnco  36179  trlcoabs  36181  trlcoabs2N  36182  trlcocnvat  36184  trlconid  36185  trlcolem  36186  trlcone  36188  cdlemg42  36189  cdlemg43  36190  cdlemg46  36195  cdlemg47  36196  tendoeq1  36224  tendoco2  36228  tendoplco2  36239  tendopltp  36240  cdlemh1  36275  cdlemh2  36276  cdlemi1  36278  cdlemi  36280  cdlemk1  36291  cdlemk2  36292  cdlemk3  36293  cdlemk4  36294  cdlemk8  36298  cdlemk9  36299  cdlemk9bN  36300  cdlemk31  36356  cdlemk32  36357  cdlemk28-3  36368  cdlemk19u  36430  cdlemk56w  36433  tendoex  36435  erngdvlem4  36451  erngdvlem4-rN  36459  dia11N  36509  dib11N  36621  cdlemn6  36663  cdlemn7  36664  cdlemn8  36665  cdlemn9  36666  dihordlem6  36674  dihordlem7  36675  dihord1  36679  dihord2a  36680  dihord2b  36681  dihord2pre  36686  dihord2pre2  36687  dihlsscpre  36695  dihvalcq2  36708  dihopelvalcpre  36709  dihord4  36719  dihord6b  36721  dihmeetlem1N  36751  dihglblem3N  36756  dihmeetlem2N  36760  dihglbcpreN  36761  dihmeetcN  36763  dihmeetbclemN  36765  dihmeetlem4preN  36767  dihjatc1  36772  dihjatc2N  36773  dihjatc3  36774  dihmeetlem9N  36776  dihmeetlem13N  36780  dihmeetlem20N  36787  dih1dimatlem0  36789  mapdpglem24  37165  mapdpglem32  37166  baerlem3lem2  37171  baerlem5alem2  37172  baerlem5blem2  37173  mapdh9aOLDN  37252  hdmap14lem6  37337
  Copyright terms: Public domain W3C validator