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

Theorem simp32 992
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 956 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  th )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl32  1037  simpr32  1046  simp132  1091  simp232  1100  simp332  1109  smogt  6400  axdc3lem4  8095  bitsfzo  12642  logfacbnd3  20478  logexprlim  20480  log2sumbnd  20709  iocinioc2  23287  totprob  23645  ax5seg  24638  cgrtr  24687  cgrtr3  24689  ofscom  24702  cgrextend  24703  segconeq  24705  ifscgr  24739  colinearxfr  24770  brofs2  24772  brifs2  24773  fscgr  24775  btwnconn1lem2  24783  btwnconn1lem9  24790  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn1lem12  24793  brsegle2  24804  seglecgr12im  24805  seglecgr12  24806  segletr  24809  outsideofeq  24825  injsurinj  25252  labs2  25293  lvsovso2  25730  icccon4  25805  tartarmap  25991  isibg1spa  26226  pdiveql  26271  ivthALT  26361  fmuldfeq  27816  lshpkrlem5  29926  lshpkrlem6  29927  atbtwnexOLDN  30258  atbtwnex  30259  4noncolr3  30264  3dimlem3a  30271  3dim1  30278  3dim2  30279  1cvrat  30287  2atjlej  30290  hlatexch4  30292  ps-2b  30293  2atm  30338  ps-2c  30339  2atmat  30372  4atlem10  30417  4atlem11b  30419  4atlem11  30420  4at  30424  4at2  30425  2lplnja  30430  2lplnj  30431  dalemswapyz  30467  dalem-ddly  30497  cdlemb  30605  paddasslem5  30635  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  4atex2-0cOLDN  30891  ltrn11at  30958  trlval3  30998  cdlemd3  31011  cdleme7aa  31053  cdleme7b  31055  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme16aN  31070  cdleme11dN  31073  cdleme11e  31074  cdleme11l  31080  cdleme11  31081  cdleme12  31082  cdleme14  31084  cdleme15a  31085  cdleme15c  31087  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17c  31099  cdleme18c  31104  cdlemeda  31109  cdlemednpq  31110  cdleme19a  31114  cdleme19c  31116  cdleme20aN  31120  cdleme20bN  31121  cdleme20l1  31131  cdleme20l2  31132  cdleme22aa  31150  cdleme22a  31151  cdleme22g  31159  cdleme23b  31161  cdleme23c  31162  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme28b  31182  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35h  31267  cdleme35sn2aw  31269  cdleme38m  31274  cdleme40n  31279  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdlemeg46gfre  31343  cdlemf1  31372  cdlemg1cex  31399  cdlemg2ce  31403  cdlemg4d  31424  cdlemg4  31428  cdlemg7fvN  31435  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg11aq  31449  cdlemg10a  31451  cdlemg12a  31454  cdlemg12b  31455  cdlemg12d  31457  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17e  31476  cdlemg17pq  31483  cdlemg17iqN  31485  cdlemg18c  31491  cdlemg18d  31492  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg28a  31504  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg28  31515  cdlemg33a  31517  cdlemg33  31522  cdlemg35  31524  cdlemg36  31525  cdlemg44a  31542  cdlemg46  31546  cdlemh2  31627  cdlemh  31628  cdlemj1  31632  cdlemk5  31647  cdlemk6  31648  cdlemki  31652  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemkole  31664  cdlemk14  31665  cdlemk16  31668  cdlemk1u  31670  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  cdlemk33N  31720  cdlemkid2  31735  cdlemkfid3N  31736  cdlemk11ta  31740  cdlemk11tc  31756  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk52  31765  cdlemk53a  31766  cdlemk54  31769  cdlemk55a  31770  cdleml1N  31787  cdleml3N  31789  cdlemn7  32015  cdlemn8  32016  cdlemn10  32018  dihordlem7  32026  dihordlem7b  32027  dihord1  32030  dihord10  32035  dihord11c  32036  dihord2  32039  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