MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp32 Structured version   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  6621  axdc3lem4  8325  bitsfzo  12939  logfacbnd3  20999  logexprlim  21001  log2sumbnd  21230  iocinioc2  24134  totprob  24677  ax5seg  25869  cgrtr  25918  cgrtr3  25920  ofscom  25933  cgrextend  25934  segconeq  25936  ifscgr  25970  colinearxfr  26001  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem2  26014  btwnconn1lem9  26021  btwnconn1lem10  26022  btwnconn1lem11  26023  btwnconn1lem12  26024  brsegle2  26035  seglecgr12im  26036  seglecgr12  26037  segletr  26040  outsideofeq  26056  ivthALT  26329  fmuldfeq  27680  lshpkrlem5  29849  lshpkrlem6  29850  atbtwnexOLDN  30181  atbtwnex  30182  4noncolr3  30187  3dimlem3a  30194  3dim1  30201  3dim2  30202  1cvrat  30210  2atjlej  30213  hlatexch4  30215  ps-2b  30216  2atm  30261  ps-2c  30262  2atmat  30295  4atlem10  30340  4atlem11b  30342  4atlem11  30343  4at  30347  4at2  30348  2lplnja  30353  2lplnj  30354  dalemswapyz  30390  dalem-ddly  30420  cdlemb  30528  paddasslem5  30558  pmodlem1  30580  dalawlem1  30605  dalawlem3  30607  dalawlem4  30608  dalawlem5  30609  dalawlem6  30610  dalawlem7  30611  dalawlem8  30612  dalawlem9  30613  dalawlem11  30615  dalawlem12  30616  dalawlem15  30619  osumcllem5N  30694  osumcllem6N  30695  lhpexle3lem  30745  lhpmcvr4N  30760  lhpmcvr6N  30762  4atexlemex6  30808  4atex2  30811  4atex2-0bOLDN  30813  4atex2-0cOLDN  30814  ltrn11at  30881  trlval3  30921  cdlemd3  30934  cdleme7aa  30976  cdleme7b  30978  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme16aN  30993  cdleme11dN  30996  cdleme11e  30997  cdleme11l  31003  cdleme11  31004  cdleme12  31005  cdleme14  31007  cdleme15a  31008  cdleme15c  31010  cdleme16c  31014  cdleme16d  31015  cdleme16e  31016  cdleme16f  31017  cdleme17c  31022  cdleme18c  31027  cdlemeda  31032  cdlemednpq  31033  cdleme19a  31037  cdleme19c  31039  cdleme20aN  31043  cdleme20bN  31044  cdleme20l1  31054  cdleme20l2  31055  cdleme22aa  31073  cdleme22a  31074  cdleme22g  31082  cdleme23b  31084  cdleme23c  31085  cdleme26fALTN  31096  cdleme26f  31097  cdleme26f2ALTN  31098  cdleme26f2  31099  cdleme28b  31105  cdleme32b  31176  cdleme32c  31177  cdleme32e  31179  cdleme35h  31190  cdleme35sn2aw  31192  cdleme38m  31197  cdleme40n  31202  cdleme41sn3aw  31208  cdleme41sn4aw  31209  cdlemeg46gfre  31266  cdlemf1  31295  cdlemg1cex  31322  cdlemg2ce  31326  cdlemg4d  31347  cdlemg4  31351  cdlemg7fvN  31358  cdlemg8b  31362  cdlemg8c  31363  cdlemg9a  31366  cdlemg11aq  31372  cdlemg10a  31374  cdlemg12a  31377  cdlemg12b  31378  cdlemg12d  31380  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg13  31386  cdlemg14f  31387  cdlemg14g  31388  cdlemg17b  31396  cdlemg17dN  31397  cdlemg17e  31399  cdlemg17pq  31406  cdlemg17iqN  31408  cdlemg18c  31414  cdlemg18d  31415  cdlemg19a  31417  cdlemg19  31418  cdlemg21  31420  cdlemg27a  31426  cdlemg28a  31427  cdlemg31b0N  31428  cdlemg27b  31430  cdlemg31c  31433  cdlemg33b0  31435  cdlemg28  31438  cdlemg33a  31440  cdlemg33  31445  cdlemg35  31447  cdlemg36  31448  cdlemg44a  31465  cdlemg46  31469  cdlemh2  31550  cdlemh  31551  cdlemj1  31555  cdlemk5  31570  cdlemk6  31571  cdlemki  31575  cdlemksv2  31581  cdlemk7  31582  cdlemk11  31583  cdlemkole  31587  cdlemk14  31588  cdlemk16  31591  cdlemk1u  31593  cdlemk18  31602  cdlemk19  31603  cdlemk7u  31604  cdlemk11u  31605  cdlemk33N  31643  cdlemkid2  31658  cdlemkfid3N  31659  cdlemk11ta  31663  cdlemk11tc  31679  cdlemk45  31681  cdlemk46  31682  cdlemk47  31683  cdlemk52  31688  cdlemk53a  31689  cdlemk54  31692  cdlemk55a  31693  cdleml1N  31710  cdleml3N  31712  cdlemn7  31938  cdlemn8  31939  cdlemn10  31941  dihordlem7  31949  dihordlem7b  31950  dihord1  31953  dihord10  31958  dihord11c  31959  dihord2  31962  hlhilphllem  32697
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