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  5303  fsnunf  5720  f1oiso2  5851  omeulem2  6583  unxpdomlem3  7071  gruina  8442  addid2  8997  dmdcan  9472  xaddass  10571  xaddass2  10572  xlt2add  10582  xmulasslem3  10608  xadddi2  10619  xadddi2r  10620  expaddzlem  11147  expaddz  11148  expmulz  11150  expdiv  11154  modexp  11238  ccatopth2  11465  o1add  12089  o1mul  12090  o1sub  12091  prmexpb  12798  pcpremul  12898  pcdiv  12907  pcqmul  12908  pcqdiv  12912  4sqlem12  13005  f1ocpbllem  13428  ercpbl  13453  erlecpbl  13454  latjlej12  14175  latmlem12  14191  latj4  14209  latj4rot  14210  mndodcong  14859  cmn4  15110  ablsub4  15116  abladdsub4  15117  lsm4  15154  abvdom  15605  abvres  15606  abvtrivd  15607  lspsnvs  15869  lspsneu  15878  lspfixed  15883  lspexch  15884  lsmcv  15896  lspsolvlem  15897  coe1sclmulfv  16361  cnprest  17019  hausnei2  17083  isreg2  17107  cmpcld  17131  llyrest  17213  nllyrest  17214  elptr  17270  basqtop  17404  hausflimlem  17676  tmdgsum  17780  ssbl  17973  prdsxmslem2  18077  tgqioo  18308  metnrm  18368  bndth  18458  cph2ass  18650  lmmbr2  18687  iscau3  18706  bcthlem5  18752  ovolunlem2  18859  dvres2  19264  dvfsumlem2  19376  plyadd  19601  plymul  19602  coeeu  19609  coemullem  19633  aalioulem4  19717  mulcxp  20034  cxplea  20045  cxple2  20046  cxplt2  20047  cxpcn3lem  20089  angcan  20102  ang180lem5  20113  divsqrsumlem  20276  logexprlim  20466  dchrvmasumlema  20651  dchrisum0lema  20665  logdivsum  20684  log2sumbnd  20695  abvcxp  20766  padicabv  20781  gxmodid  20948  chscllem4  22221  measxun  23541  mbfmco2  23572  dedekind  24084  nofulllem5  24362  brbtwn2  24535  axcontlem4  24597  axcontlem8  24601  cgrcomim  24614  cgrcoml  24621  cgrcomr  24622  cgrdegen  24629  btwnintr  24644  btwnexch3  24645  btwnouttr2  24647  btwnouttr  24649  btwnexch  24650  btwndiff  24652  lineid  24708  idinside  24709  btwnconn1lem7  24718  btwnconn1lem8  24719  btwnconn1lem9  24720  btwnconn1lem12  24723  btwnconn1lem14  24725  btwnconn3  24728  midofsegid  24729  segcon2  24730  brsegle2  24734  btwnoutside  24750  outsideoftr  24754  outsideofeu  24756  linethru  24778  uninqs  25050  oriso  25225  islimrs3  25592  islimrs4  25593  icccon4  25713  imonclem  25824  ismonc  25825  rocatval  25970  clscnc  26021  cnres2  26494  heibor  26556  mzpsubst  26837  pellexlem5  26929  pellex  26931  pell14qrexpclnn0  26962  pellfundex  26982  qirropth  27004  monotuz  27037  expmordi  27043  congtr  27063  congmul  27065  congsub  27068  mzpcong  27070  fzmaxdif  27079  jm2.15nn0  27107  symgsssg  27419  symgfisg  27420  idomsubgmo  27525  lsmsat  29271  lkrlsp  29365  lkrlsp2  29366  lkrlsp3  29367  latm4  29496  omlspjN  29524  hlatj4  29636  4noncolr3  29715  4noncolr2  29716  4noncolr1  29717  athgt  29718  3dimlem3a  29722  3dimlem4a  29725  3dimlem4  29726  3dimlem4OLDN  29727  3dim3  29731  1cvratex  29735  hlatexch4  29743  3atlem4  29748  atcvrlln2  29781  atcvrlln  29782  lplnnlelln  29805  lvoli2  29843  lvolnlelln  29846  lvolnlelpln  29847  4atlem11b  29870  4atlem12b  29873  2lplnja  29881  2lplnj  29882  dalemyeo  29894  dath2  29999  lncvrat  30044  cdlemblem  30055  cdlemb  30056  elpaddri  30064  padd4N  30102  llnmod2i2  30125  llnexchb2  30131  dalawlem1  30133  dalawlem2  30134  pclfinN  30162  osumcllem6N  30223  pexmidlem3N  30234  lhp2lt  30263  lhp2at0  30294  lhp2atnle  30295  lhp2atne  30296  lhp2at0nle  30297  lhp2at0ne  30298  lhpelim  30299  lhpmod2i2  30300  lhpmod6i1  30301  lhple  30304  lhpat  30305  lhpat3  30308  ltrncoelN  30405  ltrncoat  30406  ltrncnv  30408  trlat  30431  trl0  30432  ltrnnidn  30436  trlnid  30441  cdlemd7  30466  cdleme0b  30474  cdleme0c  30475  cdleme0fN  30480  cdleme02N  30484  cdleme0ex1N  30485  cdleme0ex2N  30486  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme8  30512  cdleme11a  30522  cdleme17c  30550  cdleme22gb  30556  cdlemeda  30560  cdleme20k  30581  cdleme21a  30587  cdleme21d  30592  cdleme22f2  30609  cdleme22g  30610  cdleme23a  30611  cdleme23b  30612  cdleme23c  30613  cdleme24  30614  cdleme28  30635  cdlemefrs32fva1  30663  cdlemefr32sn2aw  30666  cdlemefs32sn1aw  30676  cdleme41sn3a  30695  cdleme32fva  30699  cdleme32fva1  30700  cdleme35a  30710  cdleme35b  30712  cdleme35c  30713  cdleme35f  30716  cdleme39a  30727  cdleme42a  30733  cdleme42c  30734  cdleme42b  30740  cdleme42e  30741  cdleme42f  30742  cdleme42g  30743  cdleme42h  30744  cdleme43bN  30752  cdleme46f2g2  30755  cdleme17d2  30757  cdleme17d4  30759  cdleme48fv  30761  cdleme48fvg  30762  cdleme4gfv  30769  cdlemeg46c  30775  cdlemeg46nlpq  30779  cdlemeg46gfre  30794  cdleme48d  30797  cdlemeg49lebilem  30801  cdleme50trn2  30813  cdleme50ltrn  30819  cdleme  30822  cdlemf1  30823  cdlemf  30825  trlord  30831  ltrniotacnvval  30844  ltrniotavalbN  30846  cdlemg1cex  30850  cdlemg2dN  30852  cdlemg2ce  30854  cdlemg2fvlem  30856  cdlemg2idN  30858  cdlemg2kq  30864  cdlemg2l  30865  cdlemg2m  30866  cdlemg4b2  30872  cdlemg7fvN  30886  cdlemg8a  30889  cdlemg10bALTN  30898  cdlemg11aq  30900  cdlemg12d  30908  cdlemg13a  30913  cdlemg13  30914  cdlemg14f  30915  cdlemg14g  30916  cdlemg17a  30923  cdlemg17b  30924  cdlemg27a  30954  cdlemg31b0N  30956  cdlemg31a  30959  cdlemg31b  30960  cdlemg31c  30961  ltrnco  30981  trlcoabs  30983  trlcoabs2N  30984  trlcocnvat  30986  trlconid  30987  trlcolem  30988  trlcone  30990  cdlemg42  30991  cdlemg43  30992  cdlemg46  30997  cdlemg47  30998  tendoeq1  31026  tendoco2  31030  tendoplco2  31041  tendopltp  31042  cdlemh1  31077  cdlemh2  31078  cdlemi1  31080  cdlemi  31082  cdlemk1  31093  cdlemk2  31094  cdlemk3  31095  cdlemk4  31096  cdlemk8  31100  cdlemk9  31101  cdlemk9bN  31102  cdlemk31  31158  cdlemk32  31159  cdlemk28-3  31170  cdlemk19u  31232  cdlemk56w  31235  tendoex  31237  erngdvlem4  31253  erngdvlem4-rN  31261  dia11N  31311  dib11N  31423  cdlemn6  31465  cdlemn7  31466  cdlemn8  31467  cdlemn9  31468  dihordlem6  31476  dihordlem7  31477  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord2pre  31488  dihord2pre2  31489  dihlsscpre  31497  dihvalcq2  31510  dihopelvalcpre  31511  dihord4  31521  dihord6b  31523  dihmeetlem1N  31553  dihglblem3N  31558  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetcN  31565  dihmeetbclemN  31567  dihmeetlem4preN  31569  dihjatc1  31574  dihjatc2N  31575  dihjatc3  31576  dihmeetlem9N  31578  dihmeetlem13N  31582  dihmeetlem20N  31589  dih1dimatlem0  31591  mapdpglem24  31967  mapdpglem32  31968  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  mapdh9aOLDN  32054  hdmap14lem6  32139
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