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

Theorem simp2l 981
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 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl2l  1008  simpr2l  1014  simp12l  1068  simp22l  1074  simp32l  1080  funprg  5267  fsnunf  5680  f1oiso2  5811  omeulem2  6577  unxpdomlem3  7065  gruina  8436  addid2  8991  dmdcan  9466  xaddass  10565  xaddass2  10566  xlt2add  10576  xmulasslem3  10602  xadddi2  10613  xadddi2r  10614  expaddzlem  11141  expaddz  11142  expmulz  11144  expdiv  11148  modexp  11232  ccatopth2  11459  o1add  12083  o1mul  12084  o1sub  12085  prmexpb  12792  pcpremul  12892  pcdiv  12901  pcqmul  12902  pcqdiv  12906  4sqlem12  12999  f1ocpbllem  13422  ercpbl  13447  erlecpbl  13448  latjlej12  14169  latmlem12  14185  latj4  14203  latj4rot  14204  mndodcong  14853  cmn4  15104  ablsub4  15110  abladdsub4  15111  lsm4  15148  abvdom  15599  abvres  15600  abvtrivd  15601  lspsnvs  15863  lspsneu  15872  lspfixed  15877  lspexch  15878  lsmcv  15890  lspsolvlem  15891  coe1sclmulfv  16355  cnprest  17013  hausnei2  17077  isreg2  17101  cmpcld  17125  llyrest  17207  nllyrest  17208  elptr  17264  basqtop  17398  hausflimlem  17670  tmdgsum  17774  ssbl  17967  prdsxmslem2  18071  tgqioo  18302  metnrm  18362  bndth  18452  cph2ass  18644  lmmbr2  18681  iscau3  18700  bcthlem5  18746  ovolunlem2  18853  dvres2  19258  dvfsumlem2  19370  plyadd  19595  plymul  19596  coeeu  19603  coemullem  19627  aalioulem4  19711  mulcxp  20028  cxplea  20039  cxple2  20040  cxplt2  20041  cxpcn3lem  20083  angcan  20096  ang180lem5  20107  divsqrsumlem  20270  logexprlim  20460  dchrvmasumlema  20645  dchrisum0lema  20659  logdivsum  20678  log2sumbnd  20689  abvcxp  20760  padicabv  20775  gxmodid  20940  chscllem4  22215  dedekind  23488  axfelem17  23766  brbtwn2  23943  axcontlem4  24005  axcontlem8  24009  cgrcomim  24022  cgrcoml  24029  cgrcomr  24030  cgrdegen  24037  btwnintr  24052  btwnexch3  24053  btwnouttr2  24055  btwnouttr  24057  btwnexch  24058  btwndiff  24060  lineid  24116  idinside  24117  btwnconn1lem7  24126  btwnconn1lem8  24127  btwnconn1lem9  24128  btwnconn1lem12  24131  btwnconn1lem14  24133  btwnconn3  24136  midofsegid  24137  segcon2  24138  brsegle2  24142  btwnoutside  24158  outsideoftr  24162  outsideofeu  24164  linethru  24186  uninqs  24449  oriso  24625  islimrs3  24992  islimrs4  24993  icccon4  25113  imonclem  25224  ismonc  25225  rocatval  25370  clscnc  25421  cnres2  25894  heibor  25956  mzpsubst  26237  pellexlem5  26329  pellex  26331  pell14qrexpclnn0  26362  pellfundex  26382  qirropth  26404  monotuz  26437  expmordi  26443  congtr  26463  congmul  26465  congsub  26468  mzpcong  26470  fzmaxdif  26479  jm2.15nn0  26507  symgsssg  26819  symgfisg  26820  idomsubgmo  26925  lsmsat  28477  lkrlsp  28571  lkrlsp2  28572  lkrlsp3  28573  latm4  28702  omlspjN  28730  hlatj4  28842  4noncolr3  28921  4noncolr2  28922  4noncolr1  28923  athgt  28924  3dimlem3a  28928  3dimlem4a  28931  3dimlem4  28932  3dimlem4OLDN  28933  3dim3  28937  1cvratex  28941  hlatexch4  28949  3atlem4  28954  atcvrlln2  28987  atcvrlln  28988  lplnnlelln  29011  lvoli2  29049  lvolnlelln  29052  lvolnlelpln  29053  4atlem11b  29076  4atlem12b  29079  2lplnja  29087  2lplnj  29088  dalemyeo  29100  dath2  29205  lncvrat  29250  cdlemblem  29261  cdlemb  29262  elpaddri  29270  padd4N  29308  llnmod2i2  29331  llnexchb2  29337  dalawlem1  29339  dalawlem2  29340  pclfinN  29368  osumcllem6N  29429  pexmidlem3N  29440  lhp2lt  29469  lhp2at0  29500  lhp2atnle  29501  lhp2atne  29502  lhp2at0nle  29503  lhp2at0ne  29504  lhpelim  29505  lhpmod2i2  29506  lhpmod6i1  29507  lhple  29510  lhpat  29511  lhpat3  29514  ltrncoelN  29611  ltrncoat  29612  ltrncnv  29614  trlat  29637  trl0  29638  ltrnnidn  29642  trlnid  29647  cdlemd7  29672  cdleme0b  29680  cdleme0c  29681  cdleme0fN  29686  cdleme02N  29690  cdleme0ex1N  29691  cdleme0ex2N  29692  cdleme7aa  29710  cdleme7c  29713  cdleme7d  29714  cdleme7e  29715  cdleme7ga  29716  cdleme7  29717  cdleme8  29718  cdleme11a  29728  cdleme17c  29756  cdleme22gb  29762  cdlemeda  29766  cdleme20k  29787  cdleme21a  29793  cdleme21d  29798  cdleme22f2  29815  cdleme22g  29816  cdleme23a  29817  cdleme23b  29818  cdleme23c  29819  cdleme24  29820  cdleme28  29841  cdlemefrs32fva1  29869  cdlemefr32sn2aw  29872  cdlemefs32sn1aw  29882  cdleme41sn3a  29901  cdleme32fva  29905  cdleme32fva1  29906  cdleme35a  29916  cdleme35b  29918  cdleme35c  29919  cdleme35f  29922  cdleme39a  29933  cdleme42a  29939  cdleme42c  29940  cdleme42b  29946  cdleme42e  29947  cdleme42f  29948  cdleme42g  29949  cdleme42h  29950  cdleme43bN  29958  cdleme46f2g2  29961  cdleme17d2  29963  cdleme17d4  29965  cdleme48fv  29967  cdleme48fvg  29968  cdleme4gfv  29975  cdlemeg46c  29981  cdlemeg46nlpq  29985  cdlemeg46gfre  30000  cdleme48d  30003  cdlemeg49lebilem  30007  cdleme50trn2  30019  cdleme50ltrn  30025  cdleme  30028  cdlemf1  30029  cdlemf  30031  trlord  30037  ltrniotacnvval  30050  ltrniotavalbN  30052  cdlemg1cex  30056  cdlemg2dN  30058  cdlemg2ce  30060  cdlemg2fvlem  30062  cdlemg2idN  30064  cdlemg2kq  30070  cdlemg2l  30071  cdlemg2m  30072  cdlemg4b2  30078  cdlemg7fvN  30092  cdlemg8a  30095  cdlemg10bALTN  30104  cdlemg11aq  30106  cdlemg12d  30114  cdlemg13a  30119  cdlemg13  30120  cdlemg14f  30121  cdlemg14g  30122  cdlemg17a  30129  cdlemg17b  30130  cdlemg27a  30160  cdlemg31b0N  30162  cdlemg31a  30165  cdlemg31b  30166  cdlemg31c  30167  ltrnco  30187  trlcoabs  30189  trlcoabs2N  30190  trlcocnvat  30192  trlconid  30193  trlcolem  30194  trlcone  30196  cdlemg42  30197  cdlemg43  30198  cdlemg46  30203  cdlemg47  30204  tendoeq1  30232  tendoco2  30236  tendoplco2  30247  tendopltp  30248  cdlemh1  30283  cdlemh2  30284  cdlemi1  30286  cdlemi  30288  cdlemk1  30299  cdlemk2  30300  cdlemk3  30301  cdlemk4  30302  cdlemk8  30306  cdlemk9  30307  cdlemk9bN  30308  cdlemk31  30364  cdlemk32  30365  cdlemk28-3  30376  cdlemk19u  30438  cdlemk56w  30441  tendoex  30443  erngdvlem4  30459  erngdvlem4-rN  30467  dia11N  30517  dib11N  30629  cdlemn6  30671  cdlemn7  30672  cdlemn8  30673  cdlemn9  30674  dihordlem6  30682  dihordlem7  30683  dihord1  30687  dihord2a  30688  dihord2b  30689  dihord2pre  30694  dihord2pre2  30695  dihlsscpre  30703  dihvalcq2  30716  dihopelvalcpre  30717  dihord4  30727  dihord6b  30729  dihmeetlem1N  30759  dihglblem3N  30764  dihmeetlem2N  30768  dihglbcpreN  30769  dihmeetcN  30771  dihmeetbclemN  30773  dihmeetlem4preN  30775  dihjatc1  30780  dihjatc2N  30781  dihjatc3  30782  dihmeetlem9N  30784  dihmeetlem13N  30788  dihmeetlem20N  30795  dih1dimatlem0  30797  mapdpglem24  31173  mapdpglem32  31174  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  mapdh9aOLDN  31260  hdmap14lem6  31345
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator