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

Theorem simp31 993
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 957 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ch )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl31  1038  simpr31  1047  simp131  1092  simp231  1101  simp331  1110  smogt  6588  tsmsxp  18137  log2sumbnd  21191  iocinioc2  24095  totprob  24638  ax5seg  25781  cgrtr  25830  cgrtr3  25832  ofscom  25845  cgrextend  25846  segconeq  25848  ifscgr  25882  btwnxfr  25894  colinearxfr  25913  brofs2  25915  brifs2  25916  fscgr  25918  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn1lem12  25936  seglecgr12im  25948  seglecgr12  25949  segletr  25952  outsideofeq  25968  ivthALT  26228  fmuldfeq  27580  lshpkrlem5  29597  lshpkrlem6  29598  exatleN  29886  atbtwn  29928  atbtwnexOLDN  29929  atbtwnex  29930  4noncolr3  29935  3dimlem3a  29942  3dimlem4a  29945  3dim1  29949  3dim2  29950  1cvrat  29958  2atjlej  29961  hlatexch4  29963  ps-2b  29964  2atm  30009  2atmat  30043  4atlem11b  30090  4atlem11  30091  4at  30095  4at2  30096  2lplnja  30101  2lplnj  30102  dalemswapyz  30138  dalemccnedd  30169  cdlemb  30276  paddasslem5  30306  paddasslem15  30316  pmodlem1  30328  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem15  30367  osumcllem5N  30442  osumcllem6N  30443  lhpexle3lem  30493  lhpmcvr4N  30508  lhpmcvr6N  30510  4atex2  30559  4atex2-0bOLDN  30561  4atex3  30563  ltrn11at  30629  trlval3  30669  cdlemd3  30682  cdleme0moN  30707  cdleme7aa  30724  cdleme7b  30726  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme16aN  30741  cdleme11dN  30744  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme12  30753  cdleme14  30755  cdleme15b  30757  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17c  30770  cdleme18c  30775  cdleme18d  30777  cdlemeda  30780  cdleme19a  30785  cdleme19b  30786  cdleme19c  30787  cdleme20aN  30791  cdleme20bN  30792  cdleme20d  30794  cdleme20i  30799  cdleme20j  30800  cdleme20l1  30802  cdleme20l2  30803  cdleme21d  30812  cdleme21e  30813  cdleme21f  30814  cdleme22aa  30821  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f2  30829  cdleme22g  30830  cdleme23b  30832  cdleme26eALTN  30843  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme28a  30852  cdleme28b  30853  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35h  30938  cdleme35sn2aw  30940  cdleme41sn3aw  30956  cdleme41sn4aw  30957  cdlemeg46gfre  31014  cdlemf1  31043  cdlemg1cex  31070  cdlemg2ce  31074  cdlemg4d  31095  cdlemg4e  31096  cdlemg4f  31097  cdlemg4  31099  cdlemg6d  31103  cdlemg6e  31104  cdlemg7fvN  31106  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg9b  31115  cdlemg9  31116  cdlemg11aq  31120  cdlemg10a  31122  cdlemg12a  31125  cdlemg12b  31126  cdlemg12c  31127  cdlemg12d  31128  cdlemg13  31134  cdlemg14f  31135  cdlemg14g  31136  cdlemg17b  31144  cdlemg17dN  31145  cdlemg17e  31147  cdlemg17i  31151  cdlemg17pq  31154  cdlemg17iqN  31156  cdlemg18c  31162  cdlemg18d  31163  cdlemg18  31164  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33c0  31184  cdlemg33  31193  cdlemg35  31195  cdlemg43  31212  cdlemg44a  31213  cdlemg46  31217  cdlemh2  31298  cdlemh  31299  cdlemj1  31303  cdlemk3  31315  cdlemk5  31318  cdlemk6  31319  cdlemki  31323  cdlemksv2  31329  cdlemk12  31332  cdlemk15  31337  cdlemk16  31339  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk12u  31354  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk20-2N  31374  cdlemk22  31375  cdlemk30  31376  cdlemk31  31378  cdlemk24-3  31385  cdlemkid2  31406  cdlemkfid3N  31407  cdlemk11ta  31411  cdlemkid3N  31415  cdlemk11tc  31427  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk52  31436  cdlemk53a  31437  cdlemk53b  31438  cdleml1N  31458  cdleml3N  31460  cdlemn7  31686  cdlemn10  31689  dihordlem7  31697  dihord1  31701  dihord11c  31707  dihord2  31710  hlhilphllem  32445
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator