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  6567  bitsfzo  12876  logexprlim  20878  iocinioc2  23980  ax5seg  25593  cgrtr  25642  cgrtr3  25644  ofscom  25657  segconeq  25660  btwnxfr  25706  colinearxfr  25725  fscgr  25730  btwnconn1lem1  25737  btwnconn1lem2  25738  btwnconn1lem5  25741  btwnconn1lem6  25742  btwnconn1lem8  25744  btwnconn1lem9  25745  btwnconn1lem10  25746  btwnconn1lem11  25747  btwnconn1lem12  25748  brsegle2  25759  seglecgr12im  25760  seglecgr12  25761  segletr  25764  outsideofeq  25780  fmuldfeq  27383  bnj966  28655  lshpkrlem5  29231  lshpkrlem6  29232  atbtwnexOLDN  29563  atbtwnex  29564  4noncolr3  29569  3dimlem3a  29576  3dimlem4a  29579  3dim1  29583  3dim2  29584  1cvrat  29592  2atjlej  29595  hlatexch4  29597  ps-2b  29598  2atm  29643  ps-2c  29644  lvolex3N  29654  2atmat  29677  lvolnlelpln  29701  4atlem10  29722  4atlem11b  29724  4atlem11  29725  4at  29729  4at2  29730  2lplnja  29735  2lplnj  29736  dalemclccjdd  29804  paddasslem5  29940  paddasslem15  29950  pmodlem1  29962  dalawlem1  29987  dalawlem3  29989  dalawlem4  29990  dalawlem5  29991  dalawlem6  29992  dalawlem7  29993  dalawlem8  29994  dalawlem9  29995  dalawlem11  29997  dalawlem12  29998  dalawlem15  30001  osumcllem5N  30076  osumcllem6N  30077  lhpexle3lem  30127  lhpmcvr4N  30142  lhpmcvr6N  30144  4atexlemex6  30190  4atex2  30193  4atex2-0bOLDN  30195  4atex3  30197  ltrn11at  30263  cdlemd3  30316  cdleme7aa  30358  cdleme7b  30360  cdleme7c  30361  cdleme7d  30362  cdleme7ga  30364  cdleme16aN  30375  cdleme11dN  30378  cdleme11e  30379  cdleme11l  30385  cdleme11  30386  cdleme12  30387  cdleme14  30389  cdleme15c  30392  cdleme16b  30395  cdleme16d  30397  cdleme17b  30403  cdleme17c  30404  cdleme18c  30409  cdleme18d  30411  cdlemeda  30414  cdlemednpq  30415  cdleme19a  30419  cdleme19c  30421  cdleme20aN  30425  cdleme20bN  30426  cdleme20d  30428  cdleme20f  30430  cdleme20g  30431  cdleme20j  30434  cdleme20l1  30436  cdleme21f  30448  cdleme22aa  30455  cdleme22a  30456  cdleme22cN  30458  cdleme22e  30460  cdleme22f2  30463  cdleme22g  30464  cdleme23b  30466  cdleme23c  30467  cdleme26e  30475  cdleme26fALTN  30478  cdleme26f  30479  cdleme26f2ALTN  30480  cdleme26f2  30481  cdleme28a  30486  cdleme28b  30487  cdleme32b  30558  cdleme32c  30559  cdleme32e  30561  cdleme35h2  30573  cdleme38m  30579  cdleme41sn4aw  30591  cdlemf1  30677  cdlemg1cex  30704  cdlemg2ce  30708  cdlemg4d  30729  cdlemg4f  30731  cdlemg7fvN  30740  cdlemg8a  30743  cdlemg8b  30744  cdlemg8c  30745  cdlemg9a  30748  cdlemg11a  30753  cdlemg11aq  30754  cdlemg10a  30756  cdlemg11b  30758  cdlemg12a  30759  cdlemg12b  30760  cdlemg12d  30762  cdlemg12e  30763  cdlemg12f  30764  cdlemg12g  30765  cdlemg12  30766  cdlemg13a  30767  cdlemg13  30768  cdlemg14f  30769  cdlemg14g  30770  cdlemg17b  30778  cdlemg17dN  30779  cdlemg17e  30781  cdlemg17h  30784  cdlemg17pq  30788  cdlemg17iqN  30790  cdlemg18b  30795  cdlemg18c  30796  cdlemg18d  30797  cdlemg18  30798  cdlemg19  30800  cdlemg21  30802  cdlemg27a  30808  cdlemg31b0N  30810  cdlemg27b  30812  cdlemg33b0  30817  cdlemg33c0  30818  cdlemg28  30820  cdlemg33a  30822  cdlemg35  30829  cdlemg42  30845  cdlemg44a  30847  cdlemg47  30852  cdlemh2  30932  cdlemh  30933  cdlemj1  30937  cdlemk3  30949  cdlemk5  30952  cdlemki  30957  cdlemksv2  30963  cdlemk7  30964  cdlemk11  30965  cdlemk12  30966  cdlemkole  30969  cdlemk14  30970  cdlemk15  30971  cdlemk16a  30972  cdlemk16  30973  cdlemkj  30979  cdlemkuv2  30983  cdlemk18  30984  cdlemk19  30985  cdlemk7u  30986  cdlemk12u  30988  cdlemkoatnle-2N  30991  cdlemk13-2N  30992  cdlemkole-2N  30993  cdlemk14-2N  30994  cdlemk15-2N  30995  cdlemk16-2N  30996  cdlemk17-2N  30997  cdlemk18-2N  31002  cdlemk19-2N  31003  cdlemk7u-2N  31004  cdlemk11u-2N  31005  cdlemk12u-2N  31006  cdlemk21-2N  31007  cdlemk20-2N  31008  cdlemk22  31009  cdlemk30  31010  cdlemk31  31012  cdlemk32  31013  cdlemk24-3  31019  cdlemkid2  31040  cdlemkfid3N  31041  cdlemk45  31063  cdlemk46  31064  cdlemk47  31065  cdlemk52  31070  cdlemk53a  31071  cdleml1N  31092  cdleml3N  31094  cdlemn7  31320  cdlemn10  31323  dihordlem7  31331  dihord1  31335  dihord2a  31336  dihord10  31340  dihord11c  31341  dihord2pre2  31343  hlhilphllem  32079
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