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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 957 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ta )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl33  1038  simpr33  1047  simp133  1092  simp233  1101  simp333  1110  smogt  6384  bitsfzo  12626  logexprlim  20464  iocinioc2  23272  ax5seg  24566  cgrtr  24615  cgrtr3  24617  ofscom  24630  segconeq  24633  btwnxfr  24679  colinearxfr  24698  fscgr  24703  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn1lem12  24721  brsegle2  24732  seglecgr12im  24733  seglecgr12  24734  segletr  24737  outsideofeq  24753  lvsovso2  25627  icccon4  25702  isibg1a5a  26124  fmuldfeq  27713  bnj966  28976  lshpkrlem5  29304  lshpkrlem6  29305  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  ps-2c  29717  lvolex3N  29727  2atmat  29750  lvolnlelpln  29774  4atlem10  29795  4atlem11b  29797  4atlem11  29798  4at  29802  4at2  29803  2lplnja  29808  2lplnj  29809  dalemclccjdd  29877  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  4atexlemex6  30263  4atex2  30266  4atex2-0bOLDN  30268  4atex3  30270  ltrn11at  30336  cdlemd3  30389  cdleme7aa  30431  cdleme7b  30433  cdleme7c  30434  cdleme7d  30435  cdleme7ga  30437  cdleme16aN  30448  cdleme11dN  30451  cdleme11e  30452  cdleme11l  30458  cdleme11  30459  cdleme12  30460  cdleme14  30462  cdleme15c  30465  cdleme16b  30468  cdleme16d  30470  cdleme17b  30476  cdleme17c  30477  cdleme18c  30482  cdleme18d  30484  cdlemeda  30487  cdlemednpq  30488  cdleme19a  30492  cdleme19c  30494  cdleme20aN  30498  cdleme20bN  30499  cdleme20d  30501  cdleme20f  30503  cdleme20g  30504  cdleme20j  30507  cdleme20l1  30509  cdleme21f  30521  cdleme22aa  30528  cdleme22a  30529  cdleme22cN  30531  cdleme22e  30533  cdleme22f2  30536  cdleme22g  30537  cdleme23b  30539  cdleme23c  30540  cdleme26e  30548  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme28a  30559  cdleme28b  30560  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35h2  30646  cdleme38m  30652  cdleme41sn4aw  30664  cdlemf1  30750  cdlemg1cex  30777  cdlemg2ce  30781  cdlemg4d  30802  cdlemg4f  30804  cdlemg7fvN  30813  cdlemg8a  30816  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg11a  30826  cdlemg11aq  30827  cdlemg10a  30829  cdlemg11b  30831  cdlemg12a  30832  cdlemg12b  30833  cdlemg12d  30835  cdlemg12e  30836  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17b  30851  cdlemg17dN  30852  cdlemg17e  30854  cdlemg17h  30857  cdlemg17pq  30861  cdlemg17iqN  30863  cdlemg18b  30868  cdlemg18c  30869  cdlemg18d  30870  cdlemg18  30871  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg33b0  30890  cdlemg33c0  30891  cdlemg28  30893  cdlemg33a  30895  cdlemg35  30902  cdlemg42  30918  cdlemg44a  30920  cdlemg47  30925  cdlemh2  31005  cdlemh  31006  cdlemj1  31010  cdlemk3  31022  cdlemk5  31025  cdlemki  31030  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  cdlemkj  31052  cdlemkuv2  31056  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  cdlemk21-2N  31080  cdlemk20-2N  31081  cdlemk22  31082  cdlemk30  31083  cdlemk31  31085  cdlemk32  31086  cdlemk24-3  31092  cdlemkid2  31113  cdlemkfid3N  31114  cdlemk45  31136  cdlemk46  31137  cdlemk47  31138  cdlemk52  31143  cdlemk53a  31144  cdleml1N  31165  cdleml3N  31167  cdlemn7  31393  cdlemn10  31396  dihordlem7  31404  dihord1  31408  dihord2a  31409  dihord10  31413  dihord11c  31414  dihord2pre2  31416  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