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

Theorem simp31 991
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp31  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ch )

Proof of Theorem simp31
StepHypRef Expression
1 simp1 955 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ch )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl31  1036  simpr31  1045  simp131  1090  simp231  1099  simp331  1108  smogt  6384  tsmsxp  17837  log2sumbnd  20693  iocinioc2  23272  totprob  23630  ax5seg  24566  cgrtr  24615  cgrtr3  24617  ofscom  24630  cgrextend  24631  segconeq  24633  ifscgr  24667  btwnxfr  24679  colinearxfr  24698  brofs2  24700  brifs2  24701  fscgr  24703  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn1lem12  24721  seglecgr12im  24733  seglecgr12  24734  segletr  24737  outsideofeq  24753  labs1  25188  prdnei  25573  lvsovso2  25627  tartarmap  25888  fnctartar  25907  fnctartar2  25908  isibg1a3a  26122  ivthALT  26258  fmuldfeq  27713  lshpkrlem5  29304  lshpkrlem6  29305  exatleN  29593  atbtwn  29635  atbtwnexOLDN  29636  atbtwnex  29637  4noncolr3  29642  3dimlem3a  29649  3dimlem4a  29652  3dim1  29656  3dim2  29657  1cvrat  29665  2atjlej  29668  hlatexch4  29670  ps-2b  29671  2atm  29716  2atmat  29750  4atlem11b  29797  4atlem11  29798  4at  29802  4at2  29803  2lplnja  29808  2lplnj  29809  dalemswapyz  29845  dalemccnedd  29876  cdlemb  29983  paddasslem5  30013  paddasslem15  30023  pmodlem1  30035  dalawlem1  30060  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  dalawlem15  30074  osumcllem5N  30149  osumcllem6N  30150  lhpexle3lem  30200  lhpmcvr4N  30215  lhpmcvr6N  30217  4atex2  30266  4atex2-0bOLDN  30268  4atex3  30270  ltrn11at  30336  trlval3  30376  cdlemd3  30389  cdleme0moN  30414  cdleme7aa  30431  cdleme7b  30433  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme16aN  30448  cdleme11dN  30451  cdleme11e  30452  cdleme11l  30458  cdleme11  30459  cdleme12  30460  cdleme14  30462  cdleme15b  30464  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17c  30477  cdleme18c  30482  cdleme18d  30484  cdlemeda  30487  cdleme19a  30492  cdleme19b  30493  cdleme19c  30494  cdleme20aN  30498  cdleme20bN  30499  cdleme20d  30501  cdleme20i  30506  cdleme20j  30507  cdleme20l1  30509  cdleme20l2  30510  cdleme21d  30519  cdleme21e  30520  cdleme21f  30521  cdleme22aa  30528  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f2  30536  cdleme22g  30537  cdleme23b  30539  cdleme26eALTN  30550  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme28a  30559  cdleme28b  30560  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35h  30645  cdleme35sn2aw  30647  cdleme41sn3aw  30663  cdleme41sn4aw  30664  cdlemeg46gfre  30721  cdlemf1  30750  cdlemg1cex  30777  cdlemg2ce  30781  cdlemg4d  30802  cdlemg4e  30803  cdlemg4f  30804  cdlemg4  30806  cdlemg6d  30810  cdlemg6e  30811  cdlemg7fvN  30813  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg9  30823  cdlemg11aq  30827  cdlemg10a  30829  cdlemg12a  30832  cdlemg12b  30833  cdlemg12c  30834  cdlemg12d  30835  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17b  30851  cdlemg17dN  30852  cdlemg17e  30854  cdlemg17i  30858  cdlemg17pq  30861  cdlemg17iqN  30863  cdlemg18c  30869  cdlemg18d  30870  cdlemg18  30871  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg31c  30888  cdlemg33b0  30890  cdlemg33c0  30891  cdlemg33  30900  cdlemg35  30902  cdlemg43  30919  cdlemg44a  30920  cdlemg46  30924  cdlemh2  31005  cdlemh  31006  cdlemj1  31010  cdlemk3  31022  cdlemk5  31025  cdlemk6  31026  cdlemki  31030  cdlemksv2  31036  cdlemk12  31039  cdlemk15  31044  cdlemk16  31046  cdlemk18  31057  cdlemk19  31058  cdlemk7u  31059  cdlemk12u  31061  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk20-2N  31081  cdlemk22  31082  cdlemk30  31083  cdlemk31  31085  cdlemk24-3  31092  cdlemkid2  31113  cdlemkfid3N  31114  cdlemk11ta  31118  cdlemkid3N  31122  cdlemk11tc  31134  cdlemk45  31136  cdlemk46  31137  cdlemk47  31138  cdlemk52  31143  cdlemk53a  31144  cdlemk53b  31145  cdleml1N  31165  cdleml3N  31167  cdlemn7  31393  cdlemn10  31396  dihordlem7  31404  dihord1  31408  dihord11c  31414  dihord2  31417  hlhilphllem  32152
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