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

Theorem simp33 993
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp33  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ta )

Proof of Theorem simp33
StepHypRef Expression
1 simp3 957 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ta )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl33  1038  simpr33  1047  simp133  1092  simp233  1101  simp333  1110  smogt  6400  bitsfzo  12642  logexprlim  20480  iocinioc2  23287  ax5seg  24638  cgrtr  24687  cgrtr3  24689  ofscom  24702  segconeq  24705  btwnxfr  24751  colinearxfr  24770  fscgr  24775  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn1lem12  24793  brsegle2  24804  seglecgr12im  24805  seglecgr12  24806  segletr  24809  outsideofeq  24825  lvsovso2  25730  icccon4  25805  isibg1a5a  26227  fmuldfeq  27816  bnj966  29292  lshpkrlem5  29926  lshpkrlem6  29927  atbtwnexOLDN  30258  atbtwnex  30259  4noncolr3  30264  3dimlem3a  30271  3dimlem4a  30274  3dim1  30278  3dim2  30279  1cvrat  30287  2atjlej  30290  hlatexch4  30292  ps-2b  30293  2atm  30338  ps-2c  30339  lvolex3N  30349  2atmat  30372  lvolnlelpln  30396  4atlem10  30417  4atlem11b  30419  4atlem11  30420  4at  30424  4at2  30425  2lplnja  30430  2lplnj  30431  dalemclccjdd  30499  paddasslem5  30635  paddasslem15  30645  pmodlem1  30657  dalawlem1  30682  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  dalawlem15  30696  osumcllem5N  30771  osumcllem6N  30772  lhpexle3lem  30822  lhpmcvr4N  30837  lhpmcvr6N  30839  4atexlemex6  30885  4atex2  30888  4atex2-0bOLDN  30890  4atex3  30892  ltrn11at  30958  cdlemd3  31011  cdleme7aa  31053  cdleme7b  31055  cdleme7c  31056  cdleme7d  31057  cdleme7ga  31059  cdleme16aN  31070  cdleme11dN  31073  cdleme11e  31074  cdleme11l  31080  cdleme11  31081  cdleme12  31082  cdleme14  31084  cdleme15c  31087  cdleme16b  31090  cdleme16d  31092  cdleme17b  31098  cdleme17c  31099  cdleme18c  31104  cdleme18d  31106  cdlemeda  31109  cdlemednpq  31110  cdleme19a  31114  cdleme19c  31116  cdleme20aN  31120  cdleme20bN  31121  cdleme20d  31123  cdleme20f  31125  cdleme20g  31126  cdleme20j  31129  cdleme20l1  31131  cdleme21f  31143  cdleme22aa  31150  cdleme22a  31151  cdleme22cN  31153  cdleme22e  31155  cdleme22f2  31158  cdleme22g  31159  cdleme23b  31161  cdleme23c  31162  cdleme26e  31170  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme28a  31181  cdleme28b  31182  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35h2  31268  cdleme38m  31274  cdleme41sn4aw  31286  cdlemf1  31372  cdlemg1cex  31399  cdlemg2ce  31403  cdlemg4d  31424  cdlemg4f  31426  cdlemg7fvN  31435  cdlemg8a  31438  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg11a  31448  cdlemg11aq  31449  cdlemg10a  31451  cdlemg11b  31453  cdlemg12a  31454  cdlemg12b  31455  cdlemg12d  31457  cdlemg12e  31458  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17e  31476  cdlemg17h  31479  cdlemg17pq  31483  cdlemg17iqN  31485  cdlemg18b  31490  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg33b0  31512  cdlemg33c0  31513  cdlemg28  31515  cdlemg33a  31517  cdlemg35  31524  cdlemg42  31540  cdlemg44a  31542  cdlemg47  31547  cdlemh2  31627  cdlemh  31628  cdlemj1  31632  cdlemk3  31644  cdlemk5  31647  cdlemki  31652  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemkj  31674  cdlemkuv2  31678  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk12u  31683  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk21-2N  31702  cdlemk20-2N  31703  cdlemk22  31704  cdlemk30  31705  cdlemk31  31707  cdlemk32  31708  cdlemk24-3  31714  cdlemkid2  31735  cdlemkfid3N  31736  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk52  31765  cdlemk53a  31766  cdleml1N  31787  cdleml3N  31789  cdlemn7  32015  cdlemn10  32018  dihordlem7  32026  dihord1  32030  dihord2a  32031  dihord10  32035  dihord11c  32036  dihord2pre2  32038  hlhilphllem  32774
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