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  6620  tsmsxp  18172  log2sumbnd  21226  iocinioc2  24130  totprob  24673  ax5seg  25825  cgrtr  25874  cgrtr3  25876  ofscom  25889  cgrextend  25890  segconeq  25892  ifscgr  25926  btwnxfr  25938  colinearxfr  25957  brofs2  25959  brifs2  25960  fscgr  25962  btwnconn1lem1  25969  btwnconn1lem2  25970  btwnconn1lem5  25973  btwnconn1lem6  25974  btwnconn1lem7  25975  btwnconn1lem8  25976  btwnconn1lem9  25977  btwnconn1lem10  25978  btwnconn1lem11  25979  btwnconn1lem12  25980  seglecgr12im  25992  seglecgr12  25993  segletr  25996  outsideofeq  26012  ivthALT  26275  fmuldfeq  27627  lshpkrlem5  29751  lshpkrlem6  29752  exatleN  30040  atbtwn  30082  atbtwnexOLDN  30083  atbtwnex  30084  4noncolr3  30089  3dimlem3a  30096  3dimlem4a  30099  3dim1  30103  3dim2  30104  1cvrat  30112  2atjlej  30115  hlatexch4  30117  ps-2b  30118  2atm  30163  2atmat  30197  4atlem11b  30244  4atlem11  30245  4at  30249  4at2  30250  2lplnja  30255  2lplnj  30256  dalemswapyz  30292  dalemccnedd  30323  cdlemb  30430  paddasslem5  30460  paddasslem15  30470  pmodlem1  30482  dalawlem1  30507  dalawlem3  30509  dalawlem4  30510  dalawlem5  30511  dalawlem6  30512  dalawlem7  30513  dalawlem8  30514  dalawlem9  30515  dalawlem11  30517  dalawlem12  30518  dalawlem15  30521  osumcllem5N  30596  osumcllem6N  30597  lhpexle3lem  30647  lhpmcvr4N  30662  lhpmcvr6N  30664  4atex2  30713  4atex2-0bOLDN  30715  4atex3  30717  ltrn11at  30783  trlval3  30823  cdlemd3  30836  cdleme0moN  30861  cdleme7aa  30878  cdleme7b  30880  cdleme7c  30881  cdleme7d  30882  cdleme7e  30883  cdleme7ga  30884  cdleme7  30885  cdleme16aN  30895  cdleme11dN  30898  cdleme11e  30899  cdleme11l  30905  cdleme11  30906  cdleme12  30907  cdleme14  30909  cdleme15b  30911  cdleme15c  30912  cdleme16b  30915  cdleme16c  30916  cdleme16d  30917  cdleme16e  30918  cdleme16f  30919  cdleme17c  30924  cdleme18c  30929  cdleme18d  30931  cdlemeda  30934  cdleme19a  30939  cdleme19b  30940  cdleme19c  30941  cdleme20aN  30945  cdleme20bN  30946  cdleme20d  30948  cdleme20i  30953  cdleme20j  30954  cdleme20l1  30956  cdleme20l2  30957  cdleme21d  30966  cdleme21e  30967  cdleme21f  30968  cdleme22aa  30975  cdleme22e  30980  cdleme22eALTN  30981  cdleme22f2  30983  cdleme22g  30984  cdleme23b  30986  cdleme26eALTN  30997  cdleme26fALTN  30998  cdleme26f  30999  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme28a  31006  cdleme28b  31007  cdleme32b  31078  cdleme32c  31079  cdleme32e  31081  cdleme35h  31092  cdleme35sn2aw  31094  cdleme41sn3aw  31110  cdleme41sn4aw  31111  cdlemeg46gfre  31168  cdlemf1  31197  cdlemg1cex  31224  cdlemg2ce  31228  cdlemg4d  31249  cdlemg4e  31250  cdlemg4f  31251  cdlemg4  31253  cdlemg6d  31257  cdlemg6e  31258  cdlemg7fvN  31260  cdlemg8b  31264  cdlemg8c  31265  cdlemg9a  31268  cdlemg9b  31269  cdlemg9  31270  cdlemg11aq  31274  cdlemg10a  31276  cdlemg12a  31279  cdlemg12b  31280  cdlemg12c  31281  cdlemg12d  31282  cdlemg13  31288  cdlemg14f  31289  cdlemg14g  31290  cdlemg17b  31298  cdlemg17dN  31299  cdlemg17e  31301  cdlemg17i  31305  cdlemg17pq  31308  cdlemg17iqN  31310  cdlemg18c  31316  cdlemg18d  31317  cdlemg18  31318  cdlemg19  31320  cdlemg21  31322  cdlemg27a  31328  cdlemg31b0N  31330  cdlemg27b  31332  cdlemg31c  31335  cdlemg33b0  31337  cdlemg33c0  31338  cdlemg33  31347  cdlemg35  31349  cdlemg43  31366  cdlemg44a  31367  cdlemg46  31371  cdlemh2  31452  cdlemh  31453  cdlemj1  31457  cdlemk3  31469  cdlemk5  31472  cdlemk6  31473  cdlemki  31477  cdlemksv2  31483  cdlemk12  31486  cdlemk15  31491  cdlemk16  31493  cdlemk18  31504  cdlemk19  31505  cdlemk7u  31506  cdlemk12u  31508  cdlemkoatnle-2N  31511  cdlemk13-2N  31512  cdlemkole-2N  31513  cdlemk14-2N  31514  cdlemk15-2N  31515  cdlemk16-2N  31516  cdlemk17-2N  31517  cdlemk18-2N  31522  cdlemk19-2N  31523  cdlemk7u-2N  31524  cdlemk11u-2N  31525  cdlemk12u-2N  31526  cdlemk20-2N  31528  cdlemk22  31529  cdlemk30  31530  cdlemk31  31532  cdlemk24-3  31539  cdlemkid2  31560  cdlemkfid3N  31561  cdlemk11ta  31565  cdlemkid3N  31569  cdlemk11tc  31581  cdlemk45  31583  cdlemk46  31584  cdlemk47  31585  cdlemk52  31590  cdlemk53a  31591  cdlemk53b  31592  cdleml1N  31612  cdleml3N  31614  cdlemn7  31840  cdlemn10  31843  dihordlem7  31851  dihord1  31855  dihord11c  31861  dihord2  31864  hlhilphllem  32599
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