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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 956 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  th )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl32  1037  simpr32  1046  simp132  1091  simp232  1100  simp332  1109  smogt  6384  axdc3lem4  8079  bitsfzo  12626  logfacbnd3  20462  logexprlim  20464  log2sumbnd  20693  iocinioc2  23272  totprob  23630  ax5seg  24566  cgrtr  24615  cgrtr3  24617  ofscom  24630  cgrextend  24631  segconeq  24633  ifscgr  24667  colinearxfr  24698  brofs2  24700  brifs2  24701  fscgr  24703  btwnconn1lem2  24711  btwnconn1lem9  24718  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn1lem12  24721  brsegle2  24732  seglecgr12im  24733  seglecgr12  24734  segletr  24737  outsideofeq  24753  injsurinj  25149  labs2  25190  lvsovso2  25627  icccon4  25702  tartarmap  25888  isibg1spa  26123  pdiveql  26168  ivthALT  26258  fmuldfeq  27713  lshpkrlem5  29304  lshpkrlem6  29305  atbtwnexOLDN  29636  atbtwnex  29637  4noncolr3  29642  3dimlem3a  29649  3dim1  29656  3dim2  29657  1cvrat  29665  2atjlej  29668  hlatexch4  29670  ps-2b  29671  2atm  29716  ps-2c  29717  2atmat  29750  4atlem10  29795  4atlem11b  29797  4atlem11  29798  4at  29802  4at2  29803  2lplnja  29808  2lplnj  29809  dalemswapyz  29845  dalem-ddly  29875  cdlemb  29983  paddasslem5  30013  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  4atexlemex6  30263  4atex2  30266  4atex2-0bOLDN  30268  4atex2-0cOLDN  30269  ltrn11at  30336  trlval3  30376  cdlemd3  30389  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  cdleme15a  30463  cdleme15c  30465  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17c  30477  cdleme18c  30482  cdlemeda  30487  cdlemednpq  30488  cdleme19a  30492  cdleme19c  30494  cdleme20aN  30498  cdleme20bN  30499  cdleme20l1  30509  cdleme20l2  30510  cdleme22aa  30528  cdleme22a  30529  cdleme22g  30537  cdleme23b  30539  cdleme23c  30540  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme28b  30560  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35h  30645  cdleme35sn2aw  30647  cdleme38m  30652  cdleme40n  30657  cdleme41sn3aw  30663  cdleme41sn4aw  30664  cdlemeg46gfre  30721  cdlemf1  30750  cdlemg1cex  30777  cdlemg2ce  30781  cdlemg4d  30802  cdlemg4  30806  cdlemg7fvN  30813  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg11aq  30827  cdlemg10a  30829  cdlemg12a  30832  cdlemg12b  30833  cdlemg12d  30835  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17b  30851  cdlemg17dN  30852  cdlemg17e  30854  cdlemg17pq  30861  cdlemg17iqN  30863  cdlemg18c  30869  cdlemg18d  30870  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg28a  30882  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg31c  30888  cdlemg33b0  30890  cdlemg28  30893  cdlemg33a  30895  cdlemg33  30900  cdlemg35  30902  cdlemg36  30903  cdlemg44a  30920  cdlemg46  30924  cdlemh2  31005  cdlemh  31006  cdlemj1  31010  cdlemk5  31025  cdlemk6  31026  cdlemki  31030  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemkole  31042  cdlemk14  31043  cdlemk16  31046  cdlemk1u  31048  cdlemk18  31057  cdlemk19  31058  cdlemk7u  31059  cdlemk11u  31060  cdlemk33N  31098  cdlemkid2  31113  cdlemkfid3N  31114  cdlemk11ta  31118  cdlemk11tc  31134  cdlemk45  31136  cdlemk46  31137  cdlemk47  31138  cdlemk52  31143  cdlemk53a  31144  cdlemk54  31147  cdlemk55a  31148  cdleml1N  31165  cdleml3N  31167  cdlemn7  31393  cdlemn8  31394  cdlemn10  31396  dihordlem7  31404  dihordlem7b  31405  dihord1  31408  dihord10  31413  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