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

Theorem simp2l 1014
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 1010 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  simpl2l  1041  simpr2l  1047  simp12l  1101  simp22l  1107  simp32l  1113  funprg  5470  fsnunf  5919  f1oiso2  6046  omeulem2  7025  uniinqs  7183  unxpdomlem3  7522  gruina  8988  dedekind  9536  addid2  9555  dmdcan  10044  xaddass  11215  xaddass2  11216  xlt2add  11226  xmulasslem3  11252  xadddi2  11263  xadddi2r  11264  expaddzlem  11910  expaddz  11911  expmulz  11913  expdiv  11917  modexp  12002  ccatopth2  12368  swrdco  12468  o1add  13094  o1mul  13095  o1sub  13096  prmexpb  13806  pcpremul  13913  pcdiv  13922  pcqmul  13923  pcqdiv  13927  4sqlem12  14020  f1ocpbllem  14465  ercpbl  14490  erlecpbl  14491  latjlej12  15240  latmlem12  15256  latj4  15274  latj4rot  15275  symgsssg  15976  symgfisg  15977  mndodcong  16048  cmn4  16299  ablsub4  16305  abladdsub4  16306  lsm4  16345  abvdom  16926  abvres  16927  abvtrivd  16928  lspsnvs  17198  lspsneu  17207  lspfixed  17212  lspexch  17213  lsmcv  17225  lspsolvlem  17226  coe1sclmulfv  17739  cramerimplem3  18494  cnprest  18896  hausnei2  18960  isreg2  18984  cmpcld  19008  llyrest  19092  nllyrest  19093  elptr  19149  basqtop  19287  hausflimlem  19555  tmdgsum  19669  utop2nei  19828  trcfilu  19872  ssblps  20000  ssbl  20001  prdsxmslem2  20107  tgqioo  20380  metnrm  20441  bndth  20533  cph2ass  20734  lmmbr2  20773  iscau3  20792  bcthlem5  20842  ovolunlem2  20984  dvres2  21390  dvfsumlem2  21502  plyadd  21688  plymul  21689  coeeu  21696  coemullem  21720  aalioulem4  21804  mulcxp  22133  cxplea  22144  cxple2  22145  cxplt2  22146  cxpcn3lem  22188  angcan  22201  ang180lem5  22212  divsqrsumlem  22376  logexprlim  22567  dchrvmasumlema  22752  dchrisum0lema  22766  logdivsum  22785  log2sumbnd  22796  abvcxp  22867  padicabv  22882  tghilbert1_2  23047  brbtwn2  23154  axcontlem4  23216  axcontlem8  23220  1pthon  23493  gxmodid  23769  chscllem4  25046  orngmul  26274  measxun2  26627  measun  26628  mbfmco2  26683  probun  26805  ntrivcvgmul  27420  nofulllem5  27850  cgrcomim  28023  cgrcoml  28030  cgrcomr  28031  cgrdegen  28038  btwnintr  28053  btwnexch3  28054  btwnouttr2  28056  btwnouttr  28058  btwnexch  28059  btwndiff  28061  lineid  28117  idinside  28118  btwnconn1lem7  28127  btwnconn1lem8  28128  btwnconn1lem9  28129  btwnconn1lem12  28132  btwnconn1lem14  28134  btwnconn3  28137  midofsegid  28138  segcon2  28139  brsegle2  28143  btwnoutside  28159  outsideoftr  28163  outsideofeu  28165  linethru  28187  cnres2  28665  heibor  28723  mzpsubst  29088  pellexlem5  29177  pellex  29179  pell14qrexpclnn0  29210  pellfundex  29230  qirropth  29252  monotuz  29285  expmordi  29291  congtr  29311  congmul  29313  congsub  29316  mzpcong  29318  fzmaxdif  29327  jm2.15nn0  29355  idomsubgmo  29566  clwwlkel  30458  coe1sclmulval  30842  m1detdiag  30937  lincdifsn  30961  lsmsat  32656  lkrlsp  32750  lkrlsp2  32751  lkrlsp3  32752  latm4  32881  omlspjN  32909  hlatj4  33021  4noncolr3  33100  4noncolr2  33101  4noncolr1  33102  athgt  33103  3dimlem3a  33107  3dimlem4a  33110  3dimlem4  33111  3dimlem4OLDN  33112  3dim3  33116  1cvratex  33120  hlatexch4  33128  3atlem4  33133  atcvrlln2  33166  atcvrlln  33167  lplnnlelln  33190  lvoli2  33228  lvolnlelln  33231  lvolnlelpln  33232  4atlem11b  33255  4atlem12b  33258  2lplnja  33266  2lplnj  33267  dalemyeo  33279  dath2  33384  lncvrat  33429  cdlemblem  33440  cdlemb  33441  elpaddri  33449  padd4N  33487  llnmod2i2  33510  llnexchb2  33516  dalawlem1  33518  dalawlem2  33519  pclfinN  33547  osumcllem6N  33608  pexmidlem3N  33619  lhp2lt  33648  lhp2at0  33679  lhp2atnle  33680  lhp2atne  33681  lhp2at0nle  33682  lhp2at0ne  33683  lhpelim  33684  lhpmod2i2  33685  lhpmod6i1  33686  lhple  33689  lhpat  33690  lhpat3  33693  ltrncoelN  33790  ltrncoat  33791  ltrncnv  33793  trlat  33816  trl0  33817  ltrnnidn  33821  trlnid  33826  cdlemd7  33851  cdleme0b  33859  cdleme0c  33860  cdleme0fN  33865  cdleme02N  33869  cdleme0ex1N  33870  cdleme0ex2N  33871  cdleme7aa  33889  cdleme7c  33892  cdleme7d  33893  cdleme7e  33894  cdleme7ga  33895  cdleme7  33896  cdleme8  33897  cdleme11a  33907  cdleme17c  33935  cdleme22gb  33941  cdlemeda  33945  cdleme20k  33966  cdleme21a  33972  cdleme21d  33977  cdleme22f2  33994  cdleme22g  33995  cdleme23a  33996  cdleme23b  33997  cdleme23c  33998  cdleme24  33999  cdleme28  34020  cdlemefrs32fva1  34048  cdlemefr32sn2aw  34051  cdlemefs32sn1aw  34061  cdleme41sn3a  34080  cdleme32fva  34084  cdleme32fva1  34085  cdleme35a  34095  cdleme35b  34097  cdleme35c  34098  cdleme35f  34101  cdleme39a  34112  cdleme42a  34118  cdleme42c  34119  cdleme42b  34125  cdleme42e  34126  cdleme42f  34127  cdleme42g  34128  cdleme42h  34129  cdleme43bN  34137  cdleme46f2g2  34140  cdleme17d2  34142  cdleme17d4  34144  cdleme48fv  34146  cdleme48fvg  34147  cdleme4gfv  34154  cdlemeg46c  34160  cdlemeg46nlpq  34164  cdlemeg46gfre  34179  cdleme48d  34182  cdlemeg49lebilem  34186  cdleme50trn2  34198  cdleme50ltrn  34204  cdleme  34207  cdlemf1  34208  cdlemf  34210  trlord  34216  ltrniotacnvval  34229  ltrniotavalbN  34231  cdlemg1cex  34235  cdlemg2dN  34237  cdlemg2ce  34239  cdlemg2fvlem  34241  cdlemg2idN  34243  cdlemg2kq  34249  cdlemg2l  34250  cdlemg2m  34251  cdlemg4b2  34257  cdlemg7fvN  34271  cdlemg8a  34274  cdlemg10bALTN  34283  cdlemg11aq  34285  cdlemg12d  34293  cdlemg13a  34298  cdlemg13  34299  cdlemg14f  34300  cdlemg14g  34301  cdlemg17a  34308  cdlemg17b  34309  cdlemg27a  34339  cdlemg31b0N  34341  cdlemg31a  34344  cdlemg31b  34345  cdlemg31c  34346  ltrnco  34366  trlcoabs  34368  trlcoabs2N  34369  trlcocnvat  34371  trlconid  34372  trlcolem  34373  trlcone  34375  cdlemg42  34376  cdlemg43  34377  cdlemg46  34382  cdlemg47  34383  tendoeq1  34411  tendoco2  34415  tendoplco2  34426  tendopltp  34427  cdlemh1  34462  cdlemh2  34463  cdlemi1  34465  cdlemi  34467  cdlemk1  34478  cdlemk2  34479  cdlemk3  34480  cdlemk4  34481  cdlemk8  34485  cdlemk9  34486  cdlemk9bN  34487  cdlemk31  34543  cdlemk32  34544  cdlemk28-3  34555  cdlemk19u  34617  cdlemk56w  34620  tendoex  34622  erngdvlem4  34638  erngdvlem4-rN  34646  dia11N  34696  dib11N  34808  cdlemn6  34850  cdlemn7  34851  cdlemn8  34852  cdlemn9  34853  dihordlem6  34861  dihordlem7  34862  dihord1  34866  dihord2a  34867  dihord2b  34868  dihord2pre  34873  dihord2pre2  34874  dihlsscpre  34882  dihvalcq2  34895  dihopelvalcpre  34896  dihord4  34906  dihord6b  34908  dihmeetlem1N  34938  dihglblem3N  34943  dihmeetlem2N  34947  dihglbcpreN  34948  dihmeetcN  34950  dihmeetbclemN  34952  dihmeetlem4preN  34954  dihjatc1  34959  dihjatc2N  34960  dihjatc3  34961  dihmeetlem9N  34963  dihmeetlem13N  34967  dihmeetlem20N  34974  dih1dimatlem0  34976  mapdpglem24  35352  mapdpglem32  35353  baerlem3lem2  35358  baerlem5alem2  35359  baerlem5blem2  35360  mapdh9aOLDN  35439  hdmap14lem6  35524
  Copyright terms: Public domain W3C validator