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  6400  tsmsxp  17853  log2sumbnd  20709  iocinioc2  23287  totprob  23645  ax5seg  24638  cgrtr  24687  cgrtr3  24689  ofscom  24702  cgrextend  24703  segconeq  24705  ifscgr  24739  btwnxfr  24751  colinearxfr  24770  brofs2  24772  brifs2  24773  fscgr  24775  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn1lem12  24793  seglecgr12im  24805  seglecgr12  24806  segletr  24809  outsideofeq  24825  labs1  25291  prdnei  25676  lvsovso2  25730  tartarmap  25991  fnctartar  26010  fnctartar2  26011  isibg1a3a  26225  ivthALT  26361  fmuldfeq  27816  lshpkrlem5  29926  lshpkrlem6  29927  exatleN  30215  atbtwn  30257  atbtwnexOLDN  30258  atbtwnex  30259  4noncolr3  30264  3dimlem3a  30271  3dimlem4a  30274  3dim1  30278  3dim2  30279  1cvrat  30287  2atjlej  30290  hlatexch4  30292  ps-2b  30293  2atm  30338  2atmat  30372  4atlem11b  30419  4atlem11  30420  4at  30424  4at2  30425  2lplnja  30430  2lplnj  30431  dalemswapyz  30467  dalemccnedd  30498  cdlemb  30605  paddasslem5  30635  paddasslem15  30645  pmodlem1  30657  dalawlem1  30682  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  dalawlem15  30696  osumcllem5N  30771  osumcllem6N  30772  lhpexle3lem  30822  lhpmcvr4N  30837  lhpmcvr6N  30839  4atex2  30888  4atex2-0bOLDN  30890  4atex3  30892  ltrn11at  30958  trlval3  30998  cdlemd3  31011  cdleme0moN  31036  cdleme7aa  31053  cdleme7b  31055  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme16aN  31070  cdleme11dN  31073  cdleme11e  31074  cdleme11l  31080  cdleme11  31081  cdleme12  31082  cdleme14  31084  cdleme15b  31086  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17c  31099  cdleme18c  31104  cdleme18d  31106  cdlemeda  31109  cdleme19a  31114  cdleme19b  31115  cdleme19c  31116  cdleme20aN  31120  cdleme20bN  31121  cdleme20d  31123  cdleme20i  31128  cdleme20j  31129  cdleme20l1  31131  cdleme20l2  31132  cdleme21d  31141  cdleme21e  31142  cdleme21f  31143  cdleme22aa  31150  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f2  31158  cdleme22g  31159  cdleme23b  31161  cdleme26eALTN  31172  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme28a  31181  cdleme28b  31182  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35h  31267  cdleme35sn2aw  31269  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdlemeg46gfre  31343  cdlemf1  31372  cdlemg1cex  31399  cdlemg2ce  31403  cdlemg4d  31424  cdlemg4e  31425  cdlemg4f  31426  cdlemg4  31428  cdlemg6d  31432  cdlemg6e  31433  cdlemg7fvN  31435  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg11aq  31449  cdlemg10a  31451  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg12d  31457  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17e  31476  cdlemg17i  31480  cdlemg17pq  31483  cdlemg17iqN  31485  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33c0  31513  cdlemg33  31522  cdlemg35  31524  cdlemg43  31541  cdlemg44a  31542  cdlemg46  31546  cdlemh2  31627  cdlemh  31628  cdlemj1  31632  cdlemk3  31644  cdlemk5  31647  cdlemk6  31648  cdlemki  31652  cdlemksv2  31658  cdlemk12  31661  cdlemk15  31666  cdlemk16  31668  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk12u  31683  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk20-2N  31703  cdlemk22  31704  cdlemk30  31705  cdlemk31  31707  cdlemk24-3  31714  cdlemkid2  31735  cdlemkfid3N  31736  cdlemk11ta  31740  cdlemkid3N  31744  cdlemk11tc  31756  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk52  31765  cdlemk53a  31766  cdlemk53b  31767  cdleml1N  31787  cdleml3N  31789  cdlemn7  32015  cdlemn10  32018  dihordlem7  32026  dihord1  32030  dihord11c  32036  dihord2  32039  hlhilphllem  32774
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