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

Theorem simp2l 984
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 445 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 980 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpl2l  1011  simpr2l  1017  simp12l  1071  simp22l  1077  simp32l  1083  funprg  5502  fsnunf  5933  f1oiso2  6074  omeulem2  6828  uniinqs  6986  unxpdomlem3  7317  gruina  8695  addid2  9251  dmdcan  9726  xaddass  10830  xaddass2  10831  xlt2add  10841  xmulasslem3  10867  xadddi2  10878  xadddi2r  10879  expaddzlem  11425  expaddz  11426  expmulz  11428  expdiv  11432  modexp  11516  ccatopth2  11779  o1add  12409  o1mul  12410  o1sub  12411  prmexpb  13119  pcpremul  13219  pcdiv  13228  pcqmul  13229  pcqdiv  13233  4sqlem12  13326  f1ocpbllem  13751  ercpbl  13776  erlecpbl  13777  latjlej12  14498  latmlem12  14514  latj4  14532  latj4rot  14533  mndodcong  15182  cmn4  15433  ablsub4  15439  abladdsub4  15440  lsm4  15477  abvdom  15928  abvres  15929  abvtrivd  15930  lspsnvs  16188  lspsneu  16197  lspfixed  16202  lspexch  16203  lsmcv  16215  lspsolvlem  16216  coe1sclmulfv  16677  cnprest  17355  hausnei2  17419  isreg2  17443  cmpcld  17467  llyrest  17550  nllyrest  17551  elptr  17607  basqtop  17745  hausflimlem  18013  tmdgsum  18127  utop2nei  18282  trcfilu  18326  ssblps  18454  ssbl  18455  prdsxmslem2  18561  tgqioo  18833  metnrm  18894  bndth  18985  cph2ass  19177  lmmbr2  19214  iscau3  19233  bcthlem5  19283  ovolunlem2  19396  dvres2  19801  dvfsumlem2  19913  plyadd  20138  plymul  20139  coeeu  20146  coemullem  20170  aalioulem4  20254  mulcxp  20578  cxplea  20589  cxple2  20590  cxplt2  20591  cxpcn3lem  20633  angcan  20646  ang180lem5  20657  divsqrsumlem  20820  logexprlim  21011  dchrvmasumlema  21196  dchrisum0lema  21210  logdivsum  21229  log2sumbnd  21240  abvcxp  21311  padicabv  21326  1pthon  21593  gxmodid  21869  chscllem4  23144  measxun2  24566  measun  24567  mbfmco2  24617  probun  24679  dedekind  25189  ntrivcvgmul  25232  nofulllem5  25663  brbtwn2  25846  axcontlem4  25908  axcontlem8  25912  cgrcomim  25925  cgrcoml  25932  cgrcomr  25933  cgrdegen  25940  btwnintr  25955  btwnexch3  25956  btwnouttr2  25958  btwnouttr  25960  btwnexch  25961  btwndiff  25963  lineid  26019  idinside  26020  btwnconn1lem7  26029  btwnconn1lem8  26030  btwnconn1lem9  26031  btwnconn1lem12  26034  btwnconn1lem14  26036  btwnconn3  26039  midofsegid  26040  segcon2  26041  brsegle2  26045  btwnoutside  26061  outsideoftr  26065  outsideofeu  26067  linethru  26089  cnres2  26474  heibor  26532  mzpsubst  26807  pellexlem5  26898  pellex  26900  pell14qrexpclnn0  26931  pellfundex  26951  qirropth  26973  monotuz  27006  expmordi  27012  congtr  27032  congmul  27034  congsub  27037  mzpcong  27039  fzmaxdif  27048  jm2.15nn0  27076  symgsssg  27387  symgfisg  27388  idomsubgmo  27493  lsmsat  29868  lkrlsp  29962  lkrlsp2  29963  lkrlsp3  29964  latm4  30093  omlspjN  30121  hlatj4  30233  4noncolr3  30312  4noncolr2  30313  4noncolr1  30314  athgt  30315  3dimlem3a  30319  3dimlem4a  30322  3dimlem4  30323  3dimlem4OLDN  30324  3dim3  30328  1cvratex  30332  hlatexch4  30340  3atlem4  30345  atcvrlln2  30378  atcvrlln  30379  lplnnlelln  30402  lvoli2  30440  lvolnlelln  30443  lvolnlelpln  30444  4atlem11b  30467  4atlem12b  30470  2lplnja  30478  2lplnj  30479  dalemyeo  30491  dath2  30596  lncvrat  30641  cdlemblem  30652  cdlemb  30653  elpaddri  30661  padd4N  30699  llnmod2i2  30722  llnexchb2  30728  dalawlem1  30730  dalawlem2  30731  pclfinN  30759  osumcllem6N  30820  pexmidlem3N  30831  lhp2lt  30860  lhp2at0  30891  lhp2atnle  30892  lhp2atne  30893  lhp2at0nle  30894  lhp2at0ne  30895  lhpelim  30896  lhpmod2i2  30897  lhpmod6i1  30898  lhple  30901  lhpat  30902  lhpat3  30905  ltrncoelN  31002  ltrncoat  31003  ltrncnv  31005  trlat  31028  trl0  31029  ltrnnidn  31033  trlnid  31038  cdlemd7  31063  cdleme0b  31071  cdleme0c  31072  cdleme0fN  31077  cdleme02N  31081  cdleme0ex1N  31082  cdleme0ex2N  31083  cdleme7aa  31101  cdleme7c  31104  cdleme7d  31105  cdleme7e  31106  cdleme7ga  31107  cdleme7  31108  cdleme8  31109  cdleme11a  31119  cdleme17c  31147  cdleme22gb  31153  cdlemeda  31157  cdleme20k  31178  cdleme21a  31184  cdleme21d  31189  cdleme22f2  31206  cdleme22g  31207  cdleme23a  31208  cdleme23b  31209  cdleme23c  31210  cdleme24  31211  cdleme28  31232  cdlemefrs32fva1  31260  cdlemefr32sn2aw  31263  cdlemefs32sn1aw  31273  cdleme41sn3a  31292  cdleme32fva  31296  cdleme32fva1  31297  cdleme35a  31307  cdleme35b  31309  cdleme35c  31310  cdleme35f  31313  cdleme39a  31324  cdleme42a  31330  cdleme42c  31331  cdleme42b  31337  cdleme42e  31338  cdleme42f  31339  cdleme42g  31340  cdleme42h  31341  cdleme43bN  31349  cdleme46f2g2  31352  cdleme17d2  31354  cdleme17d4  31356  cdleme48fv  31358  cdleme48fvg  31359  cdleme4gfv  31366  cdlemeg46c  31372  cdlemeg46nlpq  31376  cdlemeg46gfre  31391  cdleme48d  31394  cdlemeg49lebilem  31398  cdleme50trn2  31410  cdleme50ltrn  31416  cdleme  31419  cdlemf1  31420  cdlemf  31422  trlord  31428  ltrniotacnvval  31441  ltrniotavalbN  31443  cdlemg1cex  31447  cdlemg2dN  31449  cdlemg2ce  31451  cdlemg2fvlem  31453  cdlemg2idN  31455  cdlemg2kq  31461  cdlemg2l  31462  cdlemg2m  31463  cdlemg4b2  31469  cdlemg7fvN  31483  cdlemg8a  31486  cdlemg10bALTN  31495  cdlemg11aq  31497  cdlemg12d  31505  cdlemg13a  31510  cdlemg13  31511  cdlemg14f  31512  cdlemg14g  31513  cdlemg17a  31520  cdlemg17b  31521  cdlemg27a  31551  cdlemg31b0N  31553  cdlemg31a  31556  cdlemg31b  31557  cdlemg31c  31558  ltrnco  31578  trlcoabs  31580  trlcoabs2N  31581  trlcocnvat  31583  trlconid  31584  trlcolem  31585  trlcone  31587  cdlemg42  31588  cdlemg43  31589  cdlemg46  31594  cdlemg47  31595  tendoeq1  31623  tendoco2  31627  tendoplco2  31638  tendopltp  31639  cdlemh1  31674  cdlemh2  31675  cdlemi1  31677  cdlemi  31679  cdlemk1  31690  cdlemk2  31691  cdlemk3  31692  cdlemk4  31693  cdlemk8  31697  cdlemk9  31698  cdlemk9bN  31699  cdlemk31  31755  cdlemk32  31756  cdlemk28-3  31767  cdlemk19u  31829  cdlemk56w  31832  tendoex  31834  erngdvlem4  31850  erngdvlem4-rN  31858  dia11N  31908  dib11N  32020  cdlemn6  32062  cdlemn7  32063  cdlemn8  32064  cdlemn9  32065  dihordlem6  32073  dihordlem7  32074  dihord1  32078  dihord2a  32079  dihord2b  32080  dihord2pre  32085  dihord2pre2  32086  dihlsscpre  32094  dihvalcq2  32107  dihopelvalcpre  32108  dihord4  32118  dihord6b  32120  dihmeetlem1N  32150  dihglblem3N  32155  dihmeetlem2N  32159  dihglbcpreN  32160  dihmeetcN  32162  dihmeetbclemN  32164  dihmeetlem4preN  32166  dihjatc1  32171  dihjatc2N  32172  dihjatc3  32173  dihmeetlem9N  32175  dihmeetlem13N  32179  dihmeetlem20N  32186  dih1dimatlem0  32188  mapdpglem24  32564  mapdpglem32  32565  baerlem3lem2  32570  baerlem5alem2  32571  baerlem5blem2  32572  mapdh9aOLDN  32651  hdmap14lem6  32736
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator