MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp31 Structured version   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  6629  tsmsxp  18184  log2sumbnd  21238  iocinioc2  24142  totprob  24685  ax5seg  25877  cgrtr  25926  cgrtr3  25928  ofscom  25941  cgrextend  25942  segconeq  25944  ifscgr  25978  btwnxfr  25990  colinearxfr  26009  brofs2  26011  brifs2  26012  fscgr  26014  btwnconn1lem1  26021  btwnconn1lem2  26022  btwnconn1lem5  26025  btwnconn1lem6  26026  btwnconn1lem7  26027  btwnconn1lem8  26028  btwnconn1lem9  26029  btwnconn1lem10  26030  btwnconn1lem11  26031  btwnconn1lem12  26032  seglecgr12im  26044  seglecgr12  26045  segletr  26048  outsideofeq  26064  ivthALT  26338  fmuldfeq  27689  lshpkrlem5  29912  lshpkrlem6  29913  exatleN  30201  atbtwn  30243  atbtwnexOLDN  30244  atbtwnex  30245  4noncolr3  30250  3dimlem3a  30257  3dimlem4a  30260  3dim1  30264  3dim2  30265  1cvrat  30273  2atjlej  30276  hlatexch4  30278  ps-2b  30279  2atm  30324  2atmat  30358  4atlem11b  30405  4atlem11  30406  4at  30410  4at2  30411  2lplnja  30416  2lplnj  30417  dalemswapyz  30453  dalemccnedd  30484  cdlemb  30591  paddasslem5  30621  paddasslem15  30631  pmodlem1  30643  dalawlem1  30668  dalawlem3  30670  dalawlem4  30671  dalawlem5  30672  dalawlem6  30673  dalawlem7  30674  dalawlem8  30675  dalawlem9  30676  dalawlem11  30678  dalawlem12  30679  dalawlem15  30682  osumcllem5N  30757  osumcllem6N  30758  lhpexle3lem  30808  lhpmcvr4N  30823  lhpmcvr6N  30825  4atex2  30874  4atex2-0bOLDN  30876  4atex3  30878  ltrn11at  30944  trlval3  30984  cdlemd3  30997  cdleme0moN  31022  cdleme7aa  31039  cdleme7b  31041  cdleme7c  31042  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme7  31046  cdleme16aN  31056  cdleme11dN  31059  cdleme11e  31060  cdleme11l  31066  cdleme11  31067  cdleme12  31068  cdleme14  31070  cdleme15b  31072  cdleme15c  31073  cdleme16b  31076  cdleme16c  31077  cdleme16d  31078  cdleme16e  31079  cdleme16f  31080  cdleme17c  31085  cdleme18c  31090  cdleme18d  31092  cdlemeda  31095  cdleme19a  31100  cdleme19b  31101  cdleme19c  31102  cdleme20aN  31106  cdleme20bN  31107  cdleme20d  31109  cdleme20i  31114  cdleme20j  31115  cdleme20l1  31117  cdleme20l2  31118  cdleme21d  31127  cdleme21e  31128  cdleme21f  31129  cdleme22aa  31136  cdleme22e  31141  cdleme22eALTN  31142  cdleme22f2  31144  cdleme22g  31145  cdleme23b  31147  cdleme26eALTN  31158  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme28a  31167  cdleme28b  31168  cdleme32b  31239  cdleme32c  31240  cdleme32e  31242  cdleme35h  31253  cdleme35sn2aw  31255  cdleme41sn3aw  31271  cdleme41sn4aw  31272  cdlemeg46gfre  31329  cdlemf1  31358  cdlemg1cex  31385  cdlemg2ce  31389  cdlemg4d  31410  cdlemg4e  31411  cdlemg4f  31412  cdlemg4  31414  cdlemg6d  31418  cdlemg6e  31419  cdlemg7fvN  31421  cdlemg8b  31425  cdlemg8c  31426  cdlemg9a  31429  cdlemg9b  31430  cdlemg9  31431  cdlemg11aq  31435  cdlemg10a  31437  cdlemg12a  31440  cdlemg12b  31441  cdlemg12c  31442  cdlemg12d  31443  cdlemg13  31449  cdlemg14f  31450  cdlemg14g  31451  cdlemg17b  31459  cdlemg17dN  31460  cdlemg17e  31462  cdlemg17i  31466  cdlemg17pq  31469  cdlemg17iqN  31471  cdlemg18c  31477  cdlemg18d  31478  cdlemg18  31479  cdlemg19  31481  cdlemg21  31483  cdlemg27a  31489  cdlemg31b0N  31491  cdlemg27b  31493  cdlemg31c  31496  cdlemg33b0  31498  cdlemg33c0  31499  cdlemg33  31508  cdlemg35  31510  cdlemg43  31527  cdlemg44a  31528  cdlemg46  31532  cdlemh2  31613  cdlemh  31614  cdlemj1  31618  cdlemk3  31630  cdlemk5  31633  cdlemk6  31634  cdlemki  31638  cdlemksv2  31644  cdlemk12  31647  cdlemk15  31652  cdlemk16  31654  cdlemk18  31665  cdlemk19  31666  cdlemk7u  31667  cdlemk12u  31669  cdlemkoatnle-2N  31672  cdlemk13-2N  31673  cdlemkole-2N  31674  cdlemk14-2N  31675  cdlemk15-2N  31676  cdlemk16-2N  31677  cdlemk17-2N  31678  cdlemk18-2N  31683  cdlemk19-2N  31684  cdlemk7u-2N  31685  cdlemk11u-2N  31686  cdlemk12u-2N  31687  cdlemk20-2N  31689  cdlemk22  31690  cdlemk30  31691  cdlemk31  31693  cdlemk24-3  31700  cdlemkid2  31721  cdlemkfid3N  31722  cdlemk11ta  31726  cdlemkid3N  31730  cdlemk11tc  31742  cdlemk45  31744  cdlemk46  31745  cdlemk47  31746  cdlemk52  31751  cdlemk53a  31752  cdlemk53b  31753  cdleml1N  31773  cdleml3N  31775  cdlemn7  32001  cdlemn10  32004  dihordlem7  32012  dihord1  32016  dihord11c  32022  dihord2  32025  hlhilphllem  32760
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