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  6380  tsmsxp  17833  log2sumbnd  20689  ax5seg  23976  cgrtr  24025  cgrtr3  24027  ofscom  24040  cgrextend  24041  segconeq  24043  ifscgr  24077  btwnxfr  24089  colinearxfr  24108  brofs2  24110  brifs2  24111  fscgr  24113  btwnconn1lem1  24120  btwnconn1lem2  24121  btwnconn1lem5  24124  btwnconn1lem6  24125  btwnconn1lem7  24126  btwnconn1lem8  24127  btwnconn1lem9  24128  btwnconn1lem10  24129  btwnconn1lem11  24130  btwnconn1lem12  24131  seglecgr12im  24143  seglecgr12  24144  segletr  24147  outsideofeq  24163  labs1  24599  prdnei  24984  lvsovso2  25038  tartarmap  25299  fnctartar  25318  fnctartar2  25319  isibg1a3a  25533  ivthALT  25669  fmuldfeq  27124  lshpkrlem5  28583  lshpkrlem6  28584  exatleN  28872  atbtwn  28914  atbtwnexOLDN  28915  atbtwnex  28916  4noncolr3  28921  3dimlem3a  28928  3dimlem4a  28931  3dim1  28935  3dim2  28936  1cvrat  28944  2atjlej  28947  hlatexch4  28949  ps-2b  28950  2atm  28995  2atmat  29029  4atlem11b  29076  4atlem11  29077  4at  29081  4at2  29082  2lplnja  29087  2lplnj  29088  dalemswapyz  29124  dalemccnedd  29155  cdlemb  29262  paddasslem5  29292  paddasslem15  29302  pmodlem1  29314  dalawlem1  29339  dalawlem3  29341  dalawlem4  29342  dalawlem5  29343  dalawlem6  29344  dalawlem7  29345  dalawlem8  29346  dalawlem9  29347  dalawlem11  29349  dalawlem12  29350  dalawlem15  29353  osumcllem5N  29428  osumcllem6N  29429  lhpexle3lem  29479  lhpmcvr4N  29494  lhpmcvr6N  29496  4atex2  29545  4atex2-0bOLDN  29547  4atex3  29549  ltrn11at  29615  trlval3  29655  cdlemd3  29668  cdleme0moN  29693  cdleme7aa  29710  cdleme7b  29712  cdleme7c  29713  cdleme7d  29714  cdleme7e  29715  cdleme7ga  29716  cdleme7  29717  cdleme16aN  29727  cdleme11dN  29730  cdleme11e  29731  cdleme11l  29737  cdleme11  29738  cdleme12  29739  cdleme14  29741  cdleme15b  29743  cdleme15c  29744  cdleme16b  29747  cdleme16c  29748  cdleme16d  29749  cdleme16e  29750  cdleme16f  29751  cdleme17c  29756  cdleme18c  29761  cdleme18d  29763  cdlemeda  29766  cdleme19a  29771  cdleme19b  29772  cdleme19c  29773  cdleme20aN  29777  cdleme20bN  29778  cdleme20d  29780  cdleme20i  29785  cdleme20j  29786  cdleme20l1  29788  cdleme20l2  29789  cdleme21d  29798  cdleme21e  29799  cdleme21f  29800  cdleme22aa  29807  cdleme22e  29812  cdleme22eALTN  29813  cdleme22f2  29815  cdleme22g  29816  cdleme23b  29818  cdleme26eALTN  29829  cdleme26fALTN  29830  cdleme26f  29831  cdleme26f2ALTN  29832  cdleme26f2  29833  cdleme28a  29838  cdleme28b  29839  cdleme32b  29910  cdleme32c  29911  cdleme32e  29913  cdleme35h  29924  cdleme35sn2aw  29926  cdleme41sn3aw  29942  cdleme41sn4aw  29943  cdlemeg46gfre  30000  cdlemf1  30029  cdlemg1cex  30056  cdlemg2ce  30060  cdlemg4d  30081  cdlemg4e  30082  cdlemg4f  30083  cdlemg4  30085  cdlemg6d  30089  cdlemg6e  30090  cdlemg7fvN  30092  cdlemg8b  30096  cdlemg8c  30097  cdlemg9a  30100  cdlemg9b  30101  cdlemg9  30102  cdlemg11aq  30106  cdlemg10a  30108  cdlemg12a  30111  cdlemg12b  30112  cdlemg12c  30113  cdlemg12d  30114  cdlemg13  30120  cdlemg14f  30121  cdlemg14g  30122  cdlemg17b  30130  cdlemg17dN  30131  cdlemg17e  30133  cdlemg17i  30137  cdlemg17pq  30140  cdlemg17iqN  30142  cdlemg18c  30148  cdlemg18d  30149  cdlemg18  30150  cdlemg19  30152  cdlemg21  30154  cdlemg27a  30160  cdlemg31b0N  30162  cdlemg27b  30164  cdlemg31c  30167  cdlemg33b0  30169  cdlemg33c0  30170  cdlemg33  30179  cdlemg35  30181  cdlemg43  30198  cdlemg44a  30199  cdlemg46  30203  cdlemh2  30284  cdlemh  30285  cdlemj1  30289  cdlemk3  30301  cdlemk5  30304  cdlemk6  30305  cdlemki  30309  cdlemksv2  30315  cdlemk12  30318  cdlemk15  30323  cdlemk16  30325  cdlemk18  30336  cdlemk19  30337  cdlemk7u  30338  cdlemk12u  30340  cdlemkoatnle-2N  30343  cdlemk13-2N  30344  cdlemkole-2N  30345  cdlemk14-2N  30346  cdlemk15-2N  30347  cdlemk16-2N  30348  cdlemk17-2N  30349  cdlemk18-2N  30354  cdlemk19-2N  30355  cdlemk7u-2N  30356  cdlemk11u-2N  30357  cdlemk12u-2N  30358  cdlemk20-2N  30360  cdlemk22  30361  cdlemk30  30362  cdlemk31  30364  cdlemk24-3  30371  cdlemkid2  30392  cdlemkfid3N  30393  cdlemk11ta  30397  cdlemkid3N  30401  cdlemk11tc  30413  cdlemk45  30415  cdlemk46  30416  cdlemk47  30417  cdlemk52  30422  cdlemk53a  30423  cdlemk53b  30424  cdleml1N  30444  cdleml3N  30446  cdlemn7  30672  cdlemn10  30675  dihordlem7  30683  dihord1  30687  dihord11c  30693  dihord2  30696  hlhilphllem  31431
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