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  6386  tsmsxp  17839  log2sumbnd  20695  iocinioc2  23274  totprob  23632  ax5seg  24568  cgrtr  24617  cgrtr3  24619  ofscom  24632  cgrextend  24633  segconeq  24635  ifscgr  24669  btwnxfr  24681  colinearxfr  24700  brofs2  24702  brifs2  24703  fscgr  24705  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem5  24716  btwnconn1lem6  24717  btwnconn1lem7  24718  btwnconn1lem8  24719  btwnconn1lem9  24720  btwnconn1lem10  24721  btwnconn1lem11  24722  btwnconn1lem12  24723  seglecgr12im  24735  seglecgr12  24736  segletr  24739  outsideofeq  24755  labs1  25199  prdnei  25584  lvsovso2  25638  tartarmap  25899  fnctartar  25918  fnctartar2  25919  isibg1a3a  26133  ivthALT  26269  fmuldfeq  27724  lshpkrlem5  29377  lshpkrlem6  29378  exatleN  29666  atbtwn  29708  atbtwnexOLDN  29709  atbtwnex  29710  4noncolr3  29715  3dimlem3a  29722  3dimlem4a  29725  3dim1  29729  3dim2  29730  1cvrat  29738  2atjlej  29741  hlatexch4  29743  ps-2b  29744  2atm  29789  2atmat  29823  4atlem11b  29870  4atlem11  29871  4at  29875  4at2  29876  2lplnja  29881  2lplnj  29882  dalemswapyz  29918  dalemccnedd  29949  cdlemb  30056  paddasslem5  30086  paddasslem15  30096  pmodlem1  30108  dalawlem1  30133  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  dalawlem15  30147  osumcllem5N  30222  osumcllem6N  30223  lhpexle3lem  30273  lhpmcvr4N  30288  lhpmcvr6N  30290  4atex2  30339  4atex2-0bOLDN  30341  4atex3  30343  ltrn11at  30409  trlval3  30449  cdlemd3  30462  cdleme0moN  30487  cdleme7aa  30504  cdleme7b  30506  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme16aN  30521  cdleme11dN  30524  cdleme11e  30525  cdleme11l  30531  cdleme11  30532  cdleme12  30533  cdleme14  30535  cdleme15b  30537  cdleme15c  30538  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme17c  30550  cdleme18c  30555  cdleme18d  30557  cdlemeda  30560  cdleme19a  30565  cdleme19b  30566  cdleme19c  30567  cdleme20aN  30571  cdleme20bN  30572  cdleme20d  30574  cdleme20i  30579  cdleme20j  30580  cdleme20l1  30582  cdleme20l2  30583  cdleme21d  30592  cdleme21e  30593  cdleme21f  30594  cdleme22aa  30601  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f2  30609  cdleme22g  30610  cdleme23b  30612  cdleme26eALTN  30623  cdleme26fALTN  30624  cdleme26f  30625  cdleme26f2ALTN  30626  cdleme26f2  30627  cdleme28a  30632  cdleme28b  30633  cdleme32b  30704  cdleme32c  30705  cdleme32e  30707  cdleme35h  30718  cdleme35sn2aw  30720  cdleme41sn3aw  30736  cdleme41sn4aw  30737  cdlemeg46gfre  30794  cdlemf1  30823  cdlemg1cex  30850  cdlemg2ce  30854  cdlemg4d  30875  cdlemg4e  30876  cdlemg4f  30877  cdlemg4  30879  cdlemg6d  30883  cdlemg6e  30884  cdlemg7fvN  30886  cdlemg8b  30890  cdlemg8c  30891  cdlemg9a  30894  cdlemg9b  30895  cdlemg9  30896  cdlemg11aq  30900  cdlemg10a  30902  cdlemg12a  30905  cdlemg12b  30906  cdlemg12c  30907  cdlemg12d  30908  cdlemg13  30914  cdlemg14f  30915  cdlemg14g  30916  cdlemg17b  30924  cdlemg17dN  30925  cdlemg17e  30927  cdlemg17i  30931  cdlemg17pq  30934  cdlemg17iqN  30936  cdlemg18c  30942  cdlemg18d  30943  cdlemg18  30944  cdlemg19  30946  cdlemg21  30948  cdlemg27a  30954  cdlemg31b0N  30956  cdlemg27b  30958  cdlemg31c  30961  cdlemg33b0  30963  cdlemg33c0  30964  cdlemg33  30973  cdlemg35  30975  cdlemg43  30992  cdlemg44a  30993  cdlemg46  30997  cdlemh2  31078  cdlemh  31079  cdlemj1  31083  cdlemk3  31095  cdlemk5  31098  cdlemk6  31099  cdlemki  31103  cdlemksv2  31109  cdlemk12  31112  cdlemk15  31117  cdlemk16  31119  cdlemk18  31130  cdlemk19  31131  cdlemk7u  31132  cdlemk12u  31134  cdlemkoatnle-2N  31137  cdlemk13-2N  31138  cdlemkole-2N  31139  cdlemk14-2N  31140  cdlemk15-2N  31141  cdlemk16-2N  31142  cdlemk17-2N  31143  cdlemk18-2N  31148  cdlemk19-2N  31149  cdlemk7u-2N  31150  cdlemk11u-2N  31151  cdlemk12u-2N  31152  cdlemk20-2N  31154  cdlemk22  31155  cdlemk30  31156  cdlemk31  31158  cdlemk24-3  31165  cdlemkid2  31186  cdlemkfid3N  31187  cdlemk11ta  31191  cdlemkid3N  31195  cdlemk11tc  31207  cdlemk45  31209  cdlemk46  31210  cdlemk47  31211  cdlemk52  31216  cdlemk53a  31217  cdlemk53b  31218  cdleml1N  31238  cdleml3N  31240  cdlemn7  31466  cdlemn10  31469  dihordlem7  31477  dihord1  31481  dihord11c  31487  dihord2  31490  hlhilphllem  32225
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