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

Theorem simp2l 1056
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 464 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1052 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  simpl2l  1083  simpr2l  1089  simp12l  1143  simp22l  1149  simp32l  1155  funprg  5638  fsnunf  6118  f1oiso2  6261  omeulem2  7302  uniinqs  7461  unxpdomlem3  7796  gruina  9261  dedekind  9815  addid2  9834  dmdcan  10339  xaddass  11560  xaddass2  11561  xlt2add  11571  xmulasslem3  11597  xadddi2  11608  xadddi2r  11609  expaddzlem  12353  expaddz  12354  expmulz  12356  expdiv  12361  modexp  12445  ccatopth2  12881  swrdco  12993  o1add  13754  o1mul  13755  o1sub  13756  ntrivcvgmul  14035  prmexpb  14749  pcpremul  14872  pcdiv  14881  pcqmul  14882  pcqdiv  14886  4sqlem12  14979  f1ocpbllem  15508  ercpbl  15533  erlecpbl  15534  latjlej12  16391  latmlem12  16407  latj4  16425  latj4rot  16426  symgsssg  17186  symgfisg  17187  mndodcong  17269  cmn4  17527  ablsub4  17533  abladdsub4  17534  lsm4  17576  abvdom  18144  abvres  18145  abvtrivd  18146  lspsnvs  18415  lspsneu  18424  lspfixed  18429  lspexch  18430  lsmcv  18442  lspsolvlem  18443  coe1sclmulfv  18953  matvscacell  19538  m1detdiag  19699  cramerimplem3  19787  cnprest  20382  hausnei2  20446  isreg2  20470  cmpcld  20494  llyrest  20577  nllyrest  20578  elptr  20665  basqtop  20803  hausflimlem  21072  tmdgsum  21188  utop2nei  21343  trcfilu  21387  ssblps  21515  ssbl  21516  prdsxmslem2  21622  tgqioo  21896  metnrm  21972  bndth  22064  cph2ass  22268  lmmbr2  22307  iscau3  22326  bcthlem5  22374  ovolunlem2  22529  dvres2  22946  dvfsumlem2  23058  plyadd  23250  plymul  23251  coeeu  23258  coemullem  23283  aalioulem4  23370  mulcxp  23709  cxplea  23720  cxple2  23721  cxplt2  23722  cxpcn3lem  23766  angcan  23810  ang180lem5  23821  divsqrtsumlem  23984  logexprlim  24232  dchrvmasumlema  24417  dchrisum0lema  24431  logdivsum  24450  log2sumbnd  24461  abvcxp  24532  padicabv  24547  tghilberti2  24762  brbtwn2  25014  axcontlem4  25076  axcontlem8  25080  1pthon  25400  clwwlkel  25600  gxmodid  26088  chscllem4  27374  orngmul  28640  measxun2  29106  measun  29107  mbfmco2  29160  probun  29325  nofulllem5  30666  cgrcomim  30827  cgrcoml  30834  cgrcomr  30835  cgrdegen  30842  btwnintr  30857  btwnexch3  30858  btwnouttr2  30860  btwnouttr  30862  btwnexch  30863  btwndiff  30865  lineid  30921  idinside  30922  btwnconn1lem7  30931  btwnconn1lem8  30932  btwnconn1lem9  30933  btwnconn1lem12  30936  btwnconn1lem14  30938  btwnconn3  30941  midofsegid  30942  segcon2  30943  brsegle2  30947  btwnoutside  30963  outsideoftr  30967  outsideofeu  30969  linethru  30991  cnres2  32159  heibor  32217  lsmsat  32645  lkrlsp  32739  lkrlsp2  32740  lkrlsp3  32741  latm4  32870  omlspjN  32898  hlatj4  33010  4noncolr3  33089  4noncolr2  33090  4noncolr1  33091  athgt  33092  3dimlem3a  33096  3dimlem4a  33099  3dimlem4  33100  3dimlem4OLDN  33101  3dim3  33105  1cvratex  33109  hlatexch4  33117  3atlem4  33122  atcvrlln2  33155  atcvrlln  33156  lplnnlelln  33179  lvoli2  33217  lvolnlelln  33220  lvolnlelpln  33221  4atlem11b  33244  4atlem12b  33247  2lplnja  33255  2lplnj  33256  dalemyeo  33268  dath2  33373  lncvrat  33418  cdlemblem  33429  cdlemb  33430  elpaddri  33438  padd4N  33476  llnmod2i2  33499  llnexchb2  33505  dalawlem1  33507  dalawlem2  33508  pclfinN  33536  osumcllem6N  33597  pexmidlem3N  33608  lhp2lt  33637  lhp2at0  33668  lhp2atnle  33669  lhp2atne  33670  lhp2at0nle  33671  lhp2at0ne  33672  lhpelim  33673  lhpmod2i2  33674  lhpmod6i1  33675  lhple  33678  lhpat  33679  lhpat3  33682  ltrncoelN  33779  ltrncoat  33780  ltrncnv  33782  trlat  33806  trl0  33807  ltrnnidn  33811  trlnid  33816  cdlemd7  33841  cdleme0b  33849  cdleme0c  33850  cdleme0fN  33855  cdleme02N  33859  cdleme0ex1N  33860  cdleme0ex2N  33861  cdleme7aa  33879  cdleme7c  33882  cdleme7d  33883  cdleme7e  33884  cdleme7ga  33885  cdleme7  33886  cdleme8  33887  cdleme11a  33897  cdleme17c  33925  cdleme22gb  33931  cdlemeda  33935  cdleme20k  33957  cdleme21a  33963  cdleme21d  33968  cdleme22f2  33985  cdleme22g  33986  cdleme23a  33987  cdleme23b  33988  cdleme23c  33989  cdleme24  33990  cdleme28  34011  cdlemefrs32fva1  34039  cdlemefr32sn2aw  34042  cdlemefs32sn1aw  34052  cdleme41sn3a  34071  cdleme32fva  34075  cdleme32fva1  34076  cdleme35a  34086  cdleme35b  34088  cdleme35c  34089  cdleme35f  34092  cdleme39a  34103  cdleme42a  34109  cdleme42c  34110  cdleme42b  34116  cdleme42e  34117  cdleme42f  34118  cdleme42g  34119  cdleme42h  34120  cdleme43bN  34128  cdleme46f2g2  34131  cdleme17d2  34133  cdleme17d4  34135  cdleme48fv  34137  cdleme48fvg  34138  cdleme4gfv  34145  cdlemeg46c  34151  cdlemeg46nlpq  34155  cdlemeg46gfre  34170  cdleme48d  34173  cdlemeg49lebilem  34177  cdleme50trn2  34189  cdleme50ltrn  34195  cdleme  34198  cdlemf1  34199  cdlemf  34201  trlord  34207  ltrniotacnvval  34220  ltrniotavalbN  34222  cdlemg1cex  34226  cdlemg2dN  34228  cdlemg2ce  34230  cdlemg2fvlem  34232  cdlemg2idN  34234  cdlemg2kq  34240  cdlemg2l  34241  cdlemg2m  34242  cdlemg4b2  34248  cdlemg7fvN  34262  cdlemg8a  34265  cdlemg10bALTN  34274  cdlemg11aq  34276  cdlemg12d  34284  cdlemg13a  34289  cdlemg13  34290  cdlemg14f  34291  cdlemg14g  34292  cdlemg17a  34299  cdlemg17b  34300  cdlemg27a  34330  cdlemg31b0N  34332  cdlemg31a  34335  cdlemg31b  34336  cdlemg31c  34337  ltrnco  34357  trlcoabs  34359  trlcoabs2N  34360  trlcocnvat  34362  trlconid  34363  trlcolem  34364  trlcone  34366  cdlemg42  34367  cdlemg43  34368  cdlemg46  34373  cdlemg47  34374  tendoeq1  34402  tendoco2  34406  tendoplco2  34417  tendopltp  34418  cdlemh1  34453  cdlemh2  34454  cdlemi1  34456  cdlemi  34458  cdlemk1  34469  cdlemk2  34470  cdlemk3  34471  cdlemk4  34472  cdlemk8  34476  cdlemk9  34477  cdlemk9bN  34478  cdlemk31  34534  cdlemk32  34535  cdlemk28-3  34546  cdlemk19u  34608  cdlemk56w  34611  tendoex  34613  erngdvlem4  34629  erngdvlem4-rN  34637  dia11N  34687  dib11N  34799  cdlemn6  34841  cdlemn7  34842  cdlemn8  34843  cdlemn9  34844  dihordlem6  34852  dihordlem7  34853  dihord1  34857  dihord2a  34858  dihord2b  34859  dihord2pre  34864  dihord2pre2  34865  dihlsscpre  34873  dihvalcq2  34886  dihopelvalcpre  34887  dihord4  34897  dihord6b  34899  dihmeetlem1N  34929  dihglblem3N  34934  dihmeetlem2N  34938  dihglbcpreN  34939  dihmeetcN  34941  dihmeetbclemN  34943  dihmeetlem4preN  34945  dihjatc1  34950  dihjatc2N  34951  dihjatc3  34952  dihmeetlem9N  34954  dihmeetlem13N  34958  dihmeetlem20N  34965  dih1dimatlem0  34967  mapdpglem24  35343  mapdpglem32  35344  baerlem3lem2  35349  baerlem5alem2  35350  baerlem5blem2  35351  mapdh9aOLDN  35430  hdmap14lem6  35515  mzpsubst  35661  pellexlem5  35748  pellex  35750  pell14qrexpclnn0  35783  pellfundex  35805  qirropth  35827  monotuz  35860  expmordi  35866  congtr  35886  congmul  35888  congsub  35891  mzpcong  35893  fzmaxdif  35902  jm2.15nn0  35929  idomsubgmo  36143  iunrelexpmin1  36371  iunrelexpmin2  36375  trclimalb2  36389  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem48  38130  fourierdlem80  38162  lidldomn1  40429  rngccatidALTV  40499  coe1sclmulval  40685  lincdifsn  40725
  Copyright terms: Public domain W3C validator