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

Theorem simp2l 1009
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 454 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 1005 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  simpl2l  1036  simpr2l  1042  simp12l  1096  simp22l  1102  simp32l  1108  funprg  5457  fsnunf  5905  f1oiso2  6032  omeulem2  7012  uniinqs  7170  unxpdomlem3  7509  gruina  8975  dedekind  9523  addid2  9542  dmdcan  10031  xaddass  11202  xaddass2  11203  xlt2add  11213  xmulasslem3  11239  xadddi2  11250  xadddi2r  11251  expaddzlem  11893  expaddz  11894  expmulz  11896  expdiv  11900  modexp  11985  ccatopth2  12351  swrdco  12451  o1add  13077  o1mul  13078  o1sub  13079  prmexpb  13788  pcpremul  13895  pcdiv  13904  pcqmul  13905  pcqdiv  13909  4sqlem12  14002  f1ocpbllem  14447  ercpbl  14472  erlecpbl  14473  latjlej12  15222  latmlem12  15238  latj4  15256  latj4rot  15257  symgsssg  15955  symgfisg  15956  mndodcong  16027  cmn4  16278  ablsub4  16284  abladdsub4  16285  lsm4  16324  abvdom  16849  abvres  16850  abvtrivd  16851  lspsnvs  17119  lspsneu  17128  lspfixed  17133  lspexch  17134  lsmcv  17146  lspsolvlem  17147  coe1sclmulfv  17636  cramerimplem3  18335  cnprest  18737  hausnei2  18801  isreg2  18825  cmpcld  18849  llyrest  18933  nllyrest  18934  elptr  18990  basqtop  19128  hausflimlem  19396  tmdgsum  19510  utop2nei  19669  trcfilu  19713  ssblps  19841  ssbl  19842  prdsxmslem2  19948  tgqioo  20221  metnrm  20282  bndth  20374  cph2ass  20575  lmmbr2  20614  iscau3  20633  bcthlem5  20683  ovolunlem2  20825  dvres2  21231  dvfsumlem2  21343  plyadd  21572  plymul  21573  coeeu  21580  coemullem  21604  aalioulem4  21688  mulcxp  22017  cxplea  22028  cxple2  22029  cxplt2  22030  cxpcn3lem  22072  angcan  22085  ang180lem5  22096  divsqrsumlem  22260  logexprlim  22451  dchrvmasumlema  22636  dchrisum0lema  22650  logdivsum  22669  log2sumbnd  22680  abvcxp  22751  padicabv  22766  tghilbert1_2  22917  brbtwn2  22976  axcontlem4  23038  axcontlem8  23042  1pthon  23315  gxmodid  23591  chscllem4  24868  orngmul  26126  measxun2  26480  measun  26481  mbfmco2  26536  probun  26652  ntrivcvgmul  27266  nofulllem5  27696  cgrcomim  27869  cgrcoml  27876  cgrcomr  27877  cgrdegen  27884  btwnintr  27899  btwnexch3  27900  btwnouttr2  27902  btwnouttr  27904  btwnexch  27905  btwndiff  27907  lineid  27963  idinside  27964  btwnconn1lem7  27973  btwnconn1lem8  27974  btwnconn1lem9  27975  btwnconn1lem12  27978  btwnconn1lem14  27980  btwnconn3  27983  midofsegid  27984  segcon2  27985  brsegle2  27989  btwnoutside  28005  outsideoftr  28009  outsideofeu  28011  linethru  28033  cnres2  28508  heibor  28566  mzpsubst  28932  pellexlem5  29021  pellex  29023  pell14qrexpclnn0  29054  pellfundex  29074  qirropth  29096  monotuz  29129  expmordi  29135  congtr  29155  congmul  29157  congsub  29160  mzpcong  29162  fzmaxdif  29171  jm2.15nn0  29199  idomsubgmo  29410  clwwlkel  30303  coe1sclmulval  30642  m1detdiag  30683  lincdifsn  30707  lsmsat  32266  lkrlsp  32360  lkrlsp2  32361  lkrlsp3  32362  latm4  32491  omlspjN  32519  hlatj4  32631  4noncolr3  32710  4noncolr2  32711  4noncolr1  32712  athgt  32713  3dimlem3a  32717  3dimlem4a  32720  3dimlem4  32721  3dimlem4OLDN  32722  3dim3  32726  1cvratex  32730  hlatexch4  32738  3atlem4  32743  atcvrlln2  32776  atcvrlln  32777  lplnnlelln  32800  lvoli2  32838  lvolnlelln  32841  lvolnlelpln  32842  4atlem11b  32865  4atlem12b  32868  2lplnja  32876  2lplnj  32877  dalemyeo  32889  dath2  32994  lncvrat  33039  cdlemblem  33050  cdlemb  33051  elpaddri  33059  padd4N  33097  llnmod2i2  33120  llnexchb2  33126  dalawlem1  33128  dalawlem2  33129  pclfinN  33157  osumcllem6N  33218  pexmidlem3N  33229  lhp2lt  33258  lhp2at0  33289  lhp2atnle  33290  lhp2atne  33291  lhp2at0nle  33292  lhp2at0ne  33293  lhpelim  33294  lhpmod2i2  33295  lhpmod6i1  33296  lhple  33299  lhpat  33300  lhpat3  33303  ltrncoelN  33400  ltrncoat  33401  ltrncnv  33403  trlat  33426  trl0  33427  ltrnnidn  33431  trlnid  33436  cdlemd7  33461  cdleme0b  33469  cdleme0c  33470  cdleme0fN  33475  cdleme02N  33479  cdleme0ex1N  33480  cdleme0ex2N  33481  cdleme7aa  33499  cdleme7c  33502  cdleme7d  33503  cdleme7e  33504  cdleme7ga  33505  cdleme7  33506  cdleme8  33507  cdleme11a  33517  cdleme17c  33545  cdleme22gb  33551  cdlemeda  33555  cdleme20k  33576  cdleme21a  33582  cdleme21d  33587  cdleme22f2  33604  cdleme22g  33605  cdleme23a  33606  cdleme23b  33607  cdleme23c  33608  cdleme24  33609  cdleme28  33630  cdlemefrs32fva1  33658  cdlemefr32sn2aw  33661  cdlemefs32sn1aw  33671  cdleme41sn3a  33690  cdleme32fva  33694  cdleme32fva1  33695  cdleme35a  33705  cdleme35b  33707  cdleme35c  33708  cdleme35f  33711  cdleme39a  33722  cdleme42a  33728  cdleme42c  33729  cdleme42b  33735  cdleme42e  33736  cdleme42f  33737  cdleme42g  33738  cdleme42h  33739  cdleme43bN  33747  cdleme46f2g2  33750  cdleme17d2  33752  cdleme17d4  33754  cdleme48fv  33756  cdleme48fvg  33757  cdleme4gfv  33764  cdlemeg46c  33770  cdlemeg46nlpq  33774  cdlemeg46gfre  33789  cdleme48d  33792  cdlemeg49lebilem  33796  cdleme50trn2  33808  cdleme50ltrn  33814  cdleme  33817  cdlemf1  33818  cdlemf  33820  trlord  33826  ltrniotacnvval  33839  ltrniotavalbN  33841  cdlemg1cex  33845  cdlemg2dN  33847  cdlemg2ce  33849  cdlemg2fvlem  33851  cdlemg2idN  33853  cdlemg2kq  33859  cdlemg2l  33860  cdlemg2m  33861  cdlemg4b2  33867  cdlemg7fvN  33881  cdlemg8a  33884  cdlemg10bALTN  33893  cdlemg11aq  33895  cdlemg12d  33903  cdlemg13a  33908  cdlemg13  33909  cdlemg14f  33910  cdlemg14g  33911  cdlemg17a  33918  cdlemg17b  33919  cdlemg27a  33949  cdlemg31b0N  33951  cdlemg31a  33954  cdlemg31b  33955  cdlemg31c  33956  ltrnco  33976  trlcoabs  33978  trlcoabs2N  33979  trlcocnvat  33981  trlconid  33982  trlcolem  33983  trlcone  33985  cdlemg42  33986  cdlemg43  33987  cdlemg46  33992  cdlemg47  33993  tendoeq1  34021  tendoco2  34025  tendoplco2  34036  tendopltp  34037  cdlemh1  34072  cdlemh2  34073  cdlemi1  34075  cdlemi  34077  cdlemk1  34088  cdlemk2  34089  cdlemk3  34090  cdlemk4  34091  cdlemk8  34095  cdlemk9  34096  cdlemk9bN  34097  cdlemk31  34153  cdlemk32  34154  cdlemk28-3  34165  cdlemk19u  34227  cdlemk56w  34230  tendoex  34232  erngdvlem4  34248  erngdvlem4-rN  34256  dia11N  34306  dib11N  34418  cdlemn6  34460  cdlemn7  34461  cdlemn8  34462  cdlemn9  34463  dihordlem6  34471  dihordlem7  34472  dihord1  34476  dihord2a  34477  dihord2b  34478  dihord2pre  34483  dihord2pre2  34484  dihlsscpre  34492  dihvalcq2  34505  dihopelvalcpre  34506  dihord4  34516  dihord6b  34518  dihmeetlem1N  34548  dihglblem3N  34553  dihmeetlem2N  34557  dihglbcpreN  34558  dihmeetcN  34560  dihmeetbclemN  34562  dihmeetlem4preN  34564  dihjatc1  34569  dihjatc2N  34570  dihjatc3  34571  dihmeetlem9N  34573  dihmeetlem13N  34577  dihmeetlem20N  34584  dih1dimatlem0  34586  mapdpglem24  34962  mapdpglem32  34963  baerlem3lem2  34968  baerlem5alem2  34969  baerlem5blem2  34970  mapdh9aOLDN  35049  hdmap14lem6  35134
  Copyright terms: Public domain W3C validator