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

Theorem simp31 992
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 956 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ch )
213ad2ant3 979 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935
This theorem is referenced by:  simpl31  1037  simpr31  1046  simp131  1091  simp231  1100  simp331  1109  smogt  6526  tsmsxp  18050  log2sumbnd  20916  iocinioc2  23543  totprob  24133  ax5seg  25308  cgrtr  25357  cgrtr3  25359  ofscom  25372  cgrextend  25373  segconeq  25375  ifscgr  25409  btwnxfr  25421  colinearxfr  25440  brofs2  25442  brifs2  25443  fscgr  25445  btwnconn1lem1  25452  btwnconn1lem2  25453  btwnconn1lem5  25456  btwnconn1lem6  25457  btwnconn1lem7  25458  btwnconn1lem8  25459  btwnconn1lem9  25460  btwnconn1lem10  25461  btwnconn1lem11  25462  btwnconn1lem12  25463  seglecgr12im  25475  seglecgr12  25476  segletr  25479  outsideofeq  25495  ivthALT  25765  fmuldfeq  27219  lshpkrlem5  29375  lshpkrlem6  29376  exatleN  29664  atbtwn  29706  atbtwnexOLDN  29707  atbtwnex  29708  4noncolr3  29713  3dimlem3a  29720  3dimlem4a  29723  3dim1  29727  3dim2  29728  1cvrat  29736  2atjlej  29739  hlatexch4  29741  ps-2b  29742  2atm  29787  2atmat  29821  4atlem11b  29868  4atlem11  29869  4at  29873  4at2  29874  2lplnja  29879  2lplnj  29880  dalemswapyz  29916  dalemccnedd  29947  cdlemb  30054  paddasslem5  30084  paddasslem15  30094  pmodlem1  30106  dalawlem1  30131  dalawlem3  30133  dalawlem4  30134  dalawlem5  30135  dalawlem6  30136  dalawlem7  30137  dalawlem8  30138  dalawlem9  30139  dalawlem11  30141  dalawlem12  30142  dalawlem15  30145  osumcllem5N  30220  osumcllem6N  30221  lhpexle3lem  30271  lhpmcvr4N  30286  lhpmcvr6N  30288  4atex2  30337  4atex2-0bOLDN  30339  4atex3  30341  ltrn11at  30407  trlval3  30447  cdlemd3  30460  cdleme0moN  30485  cdleme7aa  30502  cdleme7b  30504  cdleme7c  30505  cdleme7d  30506  cdleme7e  30507  cdleme7ga  30508  cdleme7  30509  cdleme16aN  30519  cdleme11dN  30522  cdleme11e  30523  cdleme11l  30529  cdleme11  30530  cdleme12  30531  cdleme14  30533  cdleme15b  30535  cdleme15c  30536  cdleme16b  30539  cdleme16c  30540  cdleme16d  30541  cdleme16e  30542  cdleme16f  30543  cdleme17c  30548  cdleme18c  30553  cdleme18d  30555  cdlemeda  30558  cdleme19a  30563  cdleme19b  30564  cdleme19c  30565  cdleme20aN  30569  cdleme20bN  30570  cdleme20d  30572  cdleme20i  30577  cdleme20j  30578  cdleme20l1  30580  cdleme20l2  30581  cdleme21d  30590  cdleme21e  30591  cdleme21f  30592  cdleme22aa  30599  cdleme22e  30604  cdleme22eALTN  30605  cdleme22f2  30607  cdleme22g  30608  cdleme23b  30610  cdleme26eALTN  30621  cdleme26fALTN  30622  cdleme26f  30623  cdleme26f2ALTN  30624  cdleme26f2  30625  cdleme28a  30630  cdleme28b  30631  cdleme32b  30702  cdleme32c  30703  cdleme32e  30705  cdleme35h  30716  cdleme35sn2aw  30718  cdleme41sn3aw  30734  cdleme41sn4aw  30735  cdlemeg46gfre  30792  cdlemf1  30821  cdlemg1cex  30848  cdlemg2ce  30852  cdlemg4d  30873  cdlemg4e  30874  cdlemg4f  30875  cdlemg4  30877  cdlemg6d  30881  cdlemg6e  30882  cdlemg7fvN  30884  cdlemg8b  30888  cdlemg8c  30889  cdlemg9a  30892  cdlemg9b  30893  cdlemg9  30894  cdlemg11aq  30898  cdlemg10a  30900  cdlemg12a  30903  cdlemg12b  30904  cdlemg12c  30905  cdlemg12d  30906  cdlemg13  30912  cdlemg14f  30913  cdlemg14g  30914  cdlemg17b  30922  cdlemg17dN  30923  cdlemg17e  30925  cdlemg17i  30929  cdlemg17pq  30932  cdlemg17iqN  30934  cdlemg18c  30940  cdlemg18d  30941  cdlemg18  30942  cdlemg19  30944  cdlemg21  30946  cdlemg27a  30952  cdlemg31b0N  30954  cdlemg27b  30956  cdlemg31c  30959  cdlemg33b0  30961  cdlemg33c0  30962  cdlemg33  30971  cdlemg35  30973  cdlemg43  30990  cdlemg44a  30991  cdlemg46  30995  cdlemh2  31076  cdlemh  31077  cdlemj1  31081  cdlemk3  31093  cdlemk5  31096  cdlemk6  31097  cdlemki  31101  cdlemksv2  31107  cdlemk12  31110  cdlemk15  31115  cdlemk16  31117  cdlemk18  31128  cdlemk19  31129  cdlemk7u  31130  cdlemk12u  31132  cdlemkoatnle-2N  31135  cdlemk13-2N  31136  cdlemkole-2N  31137  cdlemk14-2N  31138  cdlemk15-2N  31139  cdlemk16-2N  31140  cdlemk17-2N  31141  cdlemk18-2N  31146  cdlemk19-2N  31147  cdlemk7u-2N  31148  cdlemk11u-2N  31149  cdlemk12u-2N  31150  cdlemk20-2N  31152  cdlemk22  31153  cdlemk30  31154  cdlemk31  31156  cdlemk24-3  31163  cdlemkid2  31184  cdlemkfid3N  31185  cdlemk11ta  31189  cdlemkid3N  31193  cdlemk11tc  31205  cdlemk45  31207  cdlemk46  31208  cdlemk47  31209  cdlemk52  31214  cdlemk53a  31215  cdlemk53b  31216  cdleml1N  31236  cdleml3N  31238  cdlemn7  31464  cdlemn10  31467  dihordlem7  31475  dihord1  31479  dihord11c  31485  dihord2  31488  hlhilphllem  32223
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 937
  Copyright terms: Public domain W3C validator