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

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

Proof of Theorem simp32
StepHypRef Expression
1 simp2 958 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  th )
213ad2ant3 980 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl32  1039  simpr32  1048  simp132  1093  simp232  1102  simp332  1111  smogt  6567  axdc3lem4  8268  bitsfzo  12876  logfacbnd3  20876  logexprlim  20878  log2sumbnd  21107  iocinioc2  23980  totprob  24466  ax5seg  25593  cgrtr  25642  cgrtr3  25644  ofscom  25657  cgrextend  25658  segconeq  25660  ifscgr  25694  colinearxfr  25725  brofs2  25727  brifs2  25728  fscgr  25730  btwnconn1lem2  25738  btwnconn1lem9  25745  btwnconn1lem10  25746  btwnconn1lem11  25747  btwnconn1lem12  25748  brsegle2  25759  seglecgr12im  25760  seglecgr12  25761  segletr  25764  outsideofeq  25780  ivthALT  26031  fmuldfeq  27383  lshpkrlem5  29231  lshpkrlem6  29232  atbtwnexOLDN  29563  atbtwnex  29564  4noncolr3  29569  3dimlem3a  29576  3dim1  29583  3dim2  29584  1cvrat  29592  2atjlej  29595  hlatexch4  29597  ps-2b  29598  2atm  29643  ps-2c  29644  2atmat  29677  4atlem10  29722  4atlem11b  29724  4atlem11  29725  4at  29729  4at2  29730  2lplnja  29735  2lplnj  29736  dalemswapyz  29772  dalem-ddly  29802  cdlemb  29910  paddasslem5  29940  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  4atex2-0cOLDN  30196  ltrn11at  30263  trlval3  30303  cdlemd3  30316  cdleme7aa  30358  cdleme7b  30360  cdleme7c  30361  cdleme7d  30362  cdleme7e  30363  cdleme7ga  30364  cdleme7  30365  cdleme16aN  30375  cdleme11dN  30378  cdleme11e  30379  cdleme11l  30385  cdleme11  30386  cdleme12  30387  cdleme14  30389  cdleme15a  30390  cdleme15c  30392  cdleme16c  30396  cdleme16d  30397  cdleme16e  30398  cdleme16f  30399  cdleme17c  30404  cdleme18c  30409  cdlemeda  30414  cdlemednpq  30415  cdleme19a  30419  cdleme19c  30421  cdleme20aN  30425  cdleme20bN  30426  cdleme20l1  30436  cdleme20l2  30437  cdleme22aa  30455  cdleme22a  30456  cdleme22g  30464  cdleme23b  30466  cdleme23c  30467  cdleme26fALTN  30478  cdleme26f  30479  cdleme26f2ALTN  30480  cdleme26f2  30481  cdleme28b  30487  cdleme32b  30558  cdleme32c  30559  cdleme32e  30561  cdleme35h  30572  cdleme35sn2aw  30574  cdleme38m  30579  cdleme40n  30584  cdleme41sn3aw  30590  cdleme41sn4aw  30591  cdlemeg46gfre  30648  cdlemf1  30677  cdlemg1cex  30704  cdlemg2ce  30708  cdlemg4d  30729  cdlemg4  30733  cdlemg7fvN  30740  cdlemg8b  30744  cdlemg8c  30745  cdlemg9a  30748  cdlemg11aq  30754  cdlemg10a  30756  cdlemg12a  30759  cdlemg12b  30760  cdlemg12d  30762  cdlemg12g  30765  cdlemg12  30766  cdlemg13a  30767  cdlemg13  30768  cdlemg14f  30769  cdlemg14g  30770  cdlemg17b  30778  cdlemg17dN  30779  cdlemg17e  30781  cdlemg17pq  30788  cdlemg17iqN  30790  cdlemg18c  30796  cdlemg18d  30797  cdlemg19a  30799  cdlemg19  30800  cdlemg21  30802  cdlemg27a  30808  cdlemg28a  30809  cdlemg31b0N  30810  cdlemg27b  30812  cdlemg31c  30815  cdlemg33b0  30817  cdlemg28  30820  cdlemg33a  30822  cdlemg33  30827  cdlemg35  30829  cdlemg36  30830  cdlemg44a  30847  cdlemg46  30851  cdlemh2  30932  cdlemh  30933  cdlemj1  30937  cdlemk5  30952  cdlemk6  30953  cdlemki  30957  cdlemksv2  30963  cdlemk7  30964  cdlemk11  30965  cdlemkole  30969  cdlemk14  30970  cdlemk16  30973  cdlemk1u  30975  cdlemk18  30984  cdlemk19  30985  cdlemk7u  30986  cdlemk11u  30987  cdlemk33N  31025  cdlemkid2  31040  cdlemkfid3N  31041  cdlemk11ta  31045  cdlemk11tc  31061  cdlemk45  31063  cdlemk46  31064  cdlemk47  31065  cdlemk52  31070  cdlemk53a  31071  cdlemk54  31074  cdlemk55a  31075  cdleml1N  31092  cdleml3N  31094  cdlemn7  31320  cdlemn8  31321  cdlemn10  31323  dihordlem7  31331  dihordlem7b  31332  dihord1  31335  dihord10  31340  dihord11c  31341  dihord2  31344  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