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

Theorem simp33 995
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 959 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ta )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl33  1040  simpr33  1049  simp133  1094  simp233  1103  simp333  1112  smogt  6588  bitsfzo  12902  logexprlim  20962  iocinioc2  24095  ax5seg  25781  cgrtr  25830  cgrtr3  25832  ofscom  25845  segconeq  25848  btwnxfr  25894  colinearxfr  25913  fscgr  25918  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn1lem12  25936  brsegle2  25947  seglecgr12im  25948  seglecgr12  25949  segletr  25952  outsideofeq  25968  fmuldfeq  27580  bnj966  29021  lshpkrlem5  29597  lshpkrlem6  29598  atbtwnexOLDN  29929  atbtwnex  29930  4noncolr3  29935  3dimlem3a  29942  3dimlem4a  29945  3dim1  29949  3dim2  29950  1cvrat  29958  2atjlej  29961  hlatexch4  29963  ps-2b  29964  2atm  30009  ps-2c  30010  lvolex3N  30020  2atmat  30043  lvolnlelpln  30067  4atlem10  30088  4atlem11b  30090  4atlem11  30091  4at  30095  4at2  30096  2lplnja  30101  2lplnj  30102  dalemclccjdd  30170  paddasslem5  30306  paddasslem15  30316  pmodlem1  30328  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem15  30367  osumcllem5N  30442  osumcllem6N  30443  lhpexle3lem  30493  lhpmcvr4N  30508  lhpmcvr6N  30510  4atexlemex6  30556  4atex2  30559  4atex2-0bOLDN  30561  4atex3  30563  ltrn11at  30629  cdlemd3  30682  cdleme7aa  30724  cdleme7b  30726  cdleme7c  30727  cdleme7d  30728  cdleme7ga  30730  cdleme16aN  30741  cdleme11dN  30744  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme12  30753  cdleme14  30755  cdleme15c  30758  cdleme16b  30761  cdleme16d  30763  cdleme17b  30769  cdleme17c  30770  cdleme18c  30775  cdleme18d  30777  cdlemeda  30780  cdlemednpq  30781  cdleme19a  30785  cdleme19c  30787  cdleme20aN  30791  cdleme20bN  30792  cdleme20d  30794  cdleme20f  30796  cdleme20g  30797  cdleme20j  30800  cdleme20l1  30802  cdleme21f  30814  cdleme22aa  30821  cdleme22a  30822  cdleme22cN  30824  cdleme22e  30826  cdleme22f2  30829  cdleme22g  30830  cdleme23b  30832  cdleme23c  30833  cdleme26e  30841  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme28a  30852  cdleme28b  30853  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35h2  30939  cdleme38m  30945  cdleme41sn4aw  30957  cdlemf1  31043  cdlemg1cex  31070  cdlemg2ce  31074  cdlemg4d  31095  cdlemg4f  31097  cdlemg7fvN  31106  cdlemg8a  31109  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg11a  31119  cdlemg11aq  31120  cdlemg10a  31122  cdlemg11b  31124  cdlemg12a  31125  cdlemg12b  31126  cdlemg12d  31128  cdlemg12e  31129  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg14f  31135  cdlemg14g  31136  cdlemg17b  31144  cdlemg17dN  31145  cdlemg17e  31147  cdlemg17h  31150  cdlemg17pq  31154  cdlemg17iqN  31156  cdlemg18b  31161  cdlemg18c  31162  cdlemg18d  31163  cdlemg18  31164  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg33b0  31183  cdlemg33c0  31184  cdlemg28  31186  cdlemg33a  31188  cdlemg35  31195  cdlemg42  31211  cdlemg44a  31213  cdlemg47  31218  cdlemh2  31298  cdlemh  31299  cdlemj1  31303  cdlemk3  31315  cdlemk5  31318  cdlemki  31323  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk16a  31338  cdlemk16  31339  cdlemkj  31345  cdlemkuv2  31349  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk12u  31354  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk21-2N  31373  cdlemk20-2N  31374  cdlemk22  31375  cdlemk30  31376  cdlemk31  31378  cdlemk32  31379  cdlemk24-3  31385  cdlemkid2  31406  cdlemkfid3N  31407  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk52  31436  cdlemk53a  31437  cdleml1N  31458  cdleml3N  31460  cdlemn7  31686  cdlemn10  31689  dihordlem7  31697  dihord1  31701  dihord2a  31702  dihord10  31706  dihord11c  31707  dihord2pre2  31709  hlhilphllem  32445
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