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  5301  fsnunf  5718  f1oiso2  5849  omeulem2  6581  unxpdomlem3  7069  gruina  8440  addid2  8995  dmdcan  9470  xaddass  10569  xaddass2  10570  xlt2add  10580  xmulasslem3  10606  xadddi2  10617  xadddi2r  10618  expaddzlem  11145  expaddz  11146  expmulz  11148  expdiv  11152  modexp  11236  ccatopth2  11463  o1add  12087  o1mul  12088  o1sub  12089  prmexpb  12796  pcpremul  12896  pcdiv  12905  pcqmul  12906  pcqdiv  12910  4sqlem12  13003  f1ocpbllem  13426  ercpbl  13451  erlecpbl  13452  latjlej12  14173  latmlem12  14189  latj4  14207  latj4rot  14208  mndodcong  14857  cmn4  15108  ablsub4  15114  abladdsub4  15115  lsm4  15152  abvdom  15603  abvres  15604  abvtrivd  15605  lspsnvs  15867  lspsneu  15876  lspfixed  15881  lspexch  15882  lsmcv  15894  lspsolvlem  15895  coe1sclmulfv  16359  cnprest  17017  hausnei2  17081  isreg2  17105  cmpcld  17129  llyrest  17211  nllyrest  17212  elptr  17268  basqtop  17402  hausflimlem  17674  tmdgsum  17778  ssbl  17971  prdsxmslem2  18075  tgqioo  18306  metnrm  18366  bndth  18456  cph2ass  18648  lmmbr2  18685  iscau3  18704  bcthlem5  18750  ovolunlem2  18857  dvres2  19262  dvfsumlem2  19374  plyadd  19599  plymul  19600  coeeu  19607  coemullem  19631  aalioulem4  19715  mulcxp  20032  cxplea  20043  cxple2  20044  cxplt2  20045  cxpcn3lem  20087  angcan  20100  ang180lem5  20111  divsqrsumlem  20274  logexprlim  20464  dchrvmasumlema  20649  dchrisum0lema  20663  logdivsum  20682  log2sumbnd  20693  abvcxp  20764  padicabv  20779  gxmodid  20946  chscllem4  22219  measxun  23539  mbfmco2  23570  dedekind  24082  nofulllem5  24360  brbtwn2  24533  axcontlem4  24595  axcontlem8  24599  cgrcomim  24612  cgrcoml  24619  cgrcomr  24620  cgrdegen  24627  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  btwnouttr  24647  btwnexch  24648  btwndiff  24650  lineid  24706  idinside  24707  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem12  24721  btwnconn1lem14  24723  btwnconn3  24726  midofsegid  24727  segcon2  24728  brsegle2  24732  btwnoutside  24748  outsideoftr  24752  outsideofeu  24754  linethru  24776  uninqs  25039  oriso  25214  islimrs3  25581  islimrs4  25582  icccon4  25702  imonclem  25813  ismonc  25814  rocatval  25959  clscnc  26010  cnres2  26483  heibor  26545  mzpsubst  26826  pellexlem5  26918  pellex  26920  pell14qrexpclnn0  26951  pellfundex  26971  qirropth  26993  monotuz  27026  expmordi  27032  congtr  27052  congmul  27054  congsub  27057  mzpcong  27059  fzmaxdif  27068  jm2.15nn0  27096  symgsssg  27408  symgfisg  27409  idomsubgmo  27514  lsmsat  29198  lkrlsp  29292  lkrlsp2  29293  lkrlsp3  29294  latm4  29423  omlspjN  29451  hlatj4  29563  4noncolr3  29642  4noncolr2  29643  4noncolr1  29644  athgt  29645  3dimlem3a  29649  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  3dim3  29658  1cvratex  29662  hlatexch4  29670  3atlem4  29675  atcvrlln2  29708  atcvrlln  29709  lplnnlelln  29732  lvoli2  29770  lvolnlelln  29773  lvolnlelpln  29774  4atlem11b  29797  4atlem12b  29800  2lplnja  29808  2lplnj  29809  dalemyeo  29821  dath2  29926  lncvrat  29971  cdlemblem  29982  cdlemb  29983  elpaddri  29991  padd4N  30029  llnmod2i2  30052  llnexchb2  30058  dalawlem1  30060  dalawlem2  30061  pclfinN  30089  osumcllem6N  30150  pexmidlem3N  30161  lhp2lt  30190  lhp2at0  30221  lhp2atnle  30222  lhp2atne  30223  lhp2at0nle  30224  lhp2at0ne  30225  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  lhple  30231  lhpat  30232  lhpat3  30235  ltrncoelN  30332  ltrncoat  30333  ltrncnv  30335  trlat  30358  trl0  30359  ltrnnidn  30363  trlnid  30368  cdlemd7  30393  cdleme0b  30401  cdleme0c  30402  cdleme0fN  30407  cdleme02N  30411  cdleme0ex1N  30412  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme8  30439  cdleme11a  30449  cdleme17c  30477  cdleme22gb  30483  cdlemeda  30487  cdleme20k  30508  cdleme21a  30514  cdleme21d  30519  cdleme22f2  30536  cdleme22g  30537  cdleme23a  30538  cdleme23b  30539  cdleme23c  30540  cdleme24  30541  cdleme28  30562  cdlemefrs32fva1  30590  cdlemefr32sn2aw  30593  cdlemefs32sn1aw  30603  cdleme41sn3a  30622  cdleme32fva  30626  cdleme32fva1  30627  cdleme35a  30637  cdleme35b  30639  cdleme35c  30640  cdleme35f  30643  cdleme39a  30654  cdleme42a  30660  cdleme42c  30661  cdleme42b  30667  cdleme42e  30668  cdleme42f  30669  cdleme42g  30670  cdleme42h  30671  cdleme43bN  30679  cdleme46f2g2  30682  cdleme17d2  30684  cdleme17d4  30686  cdleme48fv  30688  cdleme48fvg  30689  cdleme4gfv  30696  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdlemeg46gfre  30721  cdleme48d  30724  cdlemeg49lebilem  30728  cdleme50trn2  30740  cdleme50ltrn  30746  cdleme  30749  cdlemf1  30750  cdlemf  30752  trlord  30758  ltrniotacnvval  30771  ltrniotavalbN  30773  cdlemg1cex  30777  cdlemg2dN  30779  cdlemg2ce  30781  cdlemg2fvlem  30783  cdlemg2idN  30785  cdlemg2kq  30791  cdlemg2l  30792  cdlemg2m  30793  cdlemg4b2  30799  cdlemg7fvN  30813  cdlemg8a  30816  cdlemg10bALTN  30825  cdlemg11aq  30827  cdlemg12d  30835  cdlemg13a  30840  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17a  30850  cdlemg17b  30851  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg31a  30886  cdlemg31b  30887  cdlemg31c  30888  ltrnco  30908  trlcoabs  30910  trlcoabs2N  30911  trlcocnvat  30913  trlconid  30914  trlcolem  30915  trlcone  30917  cdlemg42  30918  cdlemg43  30919  cdlemg46  30924  cdlemg47  30925  tendoeq1  30953  tendoco2  30957  tendoplco2  30968  tendopltp  30969  cdlemh1  31004  cdlemh2  31005  cdlemi1  31007  cdlemi  31009  cdlemk1  31020  cdlemk2  31021  cdlemk3  31022  cdlemk4  31023  cdlemk8  31027  cdlemk9  31028  cdlemk9bN  31029  cdlemk31  31085  cdlemk32  31086  cdlemk28-3  31097  cdlemk19u  31159  cdlemk56w  31162  tendoex  31164  erngdvlem4  31180  erngdvlem4-rN  31188  dia11N  31238  dib11N  31350  cdlemn6  31392  cdlemn7  31393  cdlemn8  31394  cdlemn9  31395  dihordlem6  31403  dihordlem7  31404  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord2pre  31415  dihord2pre2  31416  dihlsscpre  31424  dihvalcq2  31437  dihopelvalcpre  31438  dihord4  31448  dihord6b  31450  dihmeetlem1N  31480  dihglblem3N  31485  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetcN  31492  dihmeetbclemN  31494  dihmeetlem4preN  31496  dihjatc1  31501  dihjatc2N  31502  dihjatc3  31503  dihmeetlem9N  31505  dihmeetlem13N  31509  dihmeetlem20N  31516  dih1dimatlem0  31518  mapdpglem24  31894  mapdpglem32  31895  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  mapdh9aOLDN  31981  hdmap14lem6  32066
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