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  6384  bitsfzo  12626  logexprlim  20464  ax5seg  23977  cgrtr  24026  cgrtr3  24028  ofscom  24041  segconeq  24044  btwnxfr  24090  colinearxfr  24109  fscgr  24114  btwnconn1lem1  24121  btwnconn1lem2  24122  btwnconn1lem5  24125  btwnconn1lem6  24126  btwnconn1lem8  24128  btwnconn1lem9  24129  btwnconn1lem10  24130  btwnconn1lem11  24131  btwnconn1lem12  24132  brsegle2  24143  seglecgr12im  24144  seglecgr12  24145  segletr  24148  outsideofeq  24164  lvsovso2  25039  icccon4  25114  isibg1a5a  25536  fmuldfeq  27125  bnj966  28349  lshpkrlem5  28677  lshpkrlem6  28678  atbtwnexOLDN  29009  atbtwnex  29010  4noncolr3  29015  3dimlem3a  29022  3dimlem4a  29025  3dim1  29029  3dim2  29030  1cvrat  29038  2atjlej  29041  hlatexch4  29043  ps-2b  29044  2atm  29089  ps-2c  29090  lvolex3N  29100  2atmat  29123  lvolnlelpln  29147  4atlem10  29168  4atlem11b  29170  4atlem11  29171  4at  29175  4at2  29176  2lplnja  29181  2lplnj  29182  dalemclccjdd  29250  paddasslem5  29386  paddasslem15  29396  pmodlem1  29408  dalawlem1  29433  dalawlem3  29435  dalawlem4  29436  dalawlem5  29437  dalawlem6  29438  dalawlem7  29439  dalawlem8  29440  dalawlem9  29441  dalawlem11  29443  dalawlem12  29444  dalawlem15  29447  osumcllem5N  29522  osumcllem6N  29523  lhpexle3lem  29573  lhpmcvr4N  29588  lhpmcvr6N  29590  4atexlemex6  29636  4atex2  29639  4atex2-0bOLDN  29641  4atex3  29643  ltrn11at  29709  cdlemd3  29762  cdleme7aa  29804  cdleme7b  29806  cdleme7c  29807  cdleme7d  29808  cdleme7ga  29810  cdleme16aN  29821  cdleme11dN  29824  cdleme11e  29825  cdleme11l  29831  cdleme11  29832  cdleme12  29833  cdleme14  29835  cdleme15c  29838  cdleme16b  29841  cdleme16d  29843  cdleme17b  29849  cdleme17c  29850  cdleme18c  29855  cdleme18d  29857  cdlemeda  29860  cdlemednpq  29861  cdleme19a  29865  cdleme19c  29867  cdleme20aN  29871  cdleme20bN  29872  cdleme20d  29874  cdleme20f  29876  cdleme20g  29877  cdleme20j  29880  cdleme20l1  29882  cdleme21f  29894  cdleme22aa  29901  cdleme22a  29902  cdleme22cN  29904  cdleme22e  29906  cdleme22f2  29909  cdleme22g  29910  cdleme23b  29912  cdleme23c  29913  cdleme26e  29921  cdleme26fALTN  29924  cdleme26f  29925  cdleme26f2ALTN  29926  cdleme26f2  29927  cdleme28a  29932  cdleme28b  29933  cdleme32b  30004  cdleme32c  30005  cdleme32e  30007  cdleme35h2  30019  cdleme38m  30025  cdleme41sn4aw  30037  cdlemf1  30123  cdlemg1cex  30150  cdlemg2ce  30154  cdlemg4d  30175  cdlemg4f  30177  cdlemg7fvN  30186  cdlemg8a  30189  cdlemg8b  30190  cdlemg8c  30191  cdlemg9a  30194  cdlemg11a  30199  cdlemg11aq  30200  cdlemg10a  30202  cdlemg11b  30204  cdlemg12a  30205  cdlemg12b  30206  cdlemg12d  30208  cdlemg12e  30209  cdlemg12f  30210  cdlemg12g  30211  cdlemg12  30212  cdlemg13a  30213  cdlemg13  30214  cdlemg14f  30215  cdlemg14g  30216  cdlemg17b  30224  cdlemg17dN  30225  cdlemg17e  30227  cdlemg17h  30230  cdlemg17pq  30234  cdlemg17iqN  30236  cdlemg18b  30241  cdlemg18c  30242  cdlemg18d  30243  cdlemg18  30244  cdlemg19  30246  cdlemg21  30248  cdlemg27a  30254  cdlemg31b0N  30256  cdlemg27b  30258  cdlemg33b0  30263  cdlemg33c0  30264  cdlemg28  30266  cdlemg33a  30268  cdlemg35  30275  cdlemg42  30291  cdlemg44a  30293  cdlemg47  30298  cdlemh2  30378  cdlemh  30379  cdlemj1  30383  cdlemk3  30395  cdlemk5  30398  cdlemki  30403  cdlemksv2  30409  cdlemk7  30410  cdlemk11  30411  cdlemk12  30412  cdlemkole  30415  cdlemk14  30416  cdlemk15  30417  cdlemk16a  30418  cdlemk16  30419  cdlemkj  30425  cdlemkuv2  30429  cdlemk18  30430  cdlemk19  30431  cdlemk7u  30432  cdlemk12u  30434  cdlemkoatnle-2N  30437  cdlemk13-2N  30438  cdlemkole-2N  30439  cdlemk14-2N  30440  cdlemk15-2N  30441  cdlemk16-2N  30442  cdlemk17-2N  30443  cdlemk18-2N  30448  cdlemk19-2N  30449  cdlemk7u-2N  30450  cdlemk11u-2N  30451  cdlemk12u-2N  30452  cdlemk21-2N  30453  cdlemk20-2N  30454  cdlemk22  30455  cdlemk30  30456  cdlemk31  30458  cdlemk32  30459  cdlemk24-3  30465  cdlemkid2  30486  cdlemkfid3N  30487  cdlemk45  30509  cdlemk46  30510  cdlemk47  30511  cdlemk52  30516  cdlemk53a  30517  cdleml1N  30538  cdleml3N  30540  cdlemn7  30766  cdlemn10  30769  dihordlem7  30777  dihord1  30781  dihord2a  30782  dihord10  30786  dihord11c  30787  dihord2pre2  30789  hlhilphllem  31525
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