MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp33 Structured version   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  6621  bitsfzo  12939  logexprlim  21001  iocinioc2  24134  ax5seg  25869  cgrtr  25918  cgrtr3  25920  ofscom  25933  segconeq  25936  btwnxfr  25982  colinearxfr  26001  fscgr  26006  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem5  26017  btwnconn1lem6  26018  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem10  26022  btwnconn1lem11  26023  btwnconn1lem12  26024  brsegle2  26035  seglecgr12im  26036  seglecgr12  26037  segletr  26040  outsideofeq  26056  fmuldfeq  27680  bnj966  29252  lshpkrlem5  29849  lshpkrlem6  29850  atbtwnexOLDN  30181  atbtwnex  30182  4noncolr3  30187  3dimlem3a  30194  3dimlem4a  30197  3dim1  30201  3dim2  30202  1cvrat  30210  2atjlej  30213  hlatexch4  30215  ps-2b  30216  2atm  30261  ps-2c  30262  lvolex3N  30272  2atmat  30295  lvolnlelpln  30319  4atlem10  30340  4atlem11b  30342  4atlem11  30343  4at  30347  4at2  30348  2lplnja  30353  2lplnj  30354  dalemclccjdd  30422  paddasslem5  30558  paddasslem15  30568  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  4atex3  30815  ltrn11at  30881  cdlemd3  30934  cdleme7aa  30976  cdleme7b  30978  cdleme7c  30979  cdleme7d  30980  cdleme7ga  30982  cdleme16aN  30993  cdleme11dN  30996  cdleme11e  30997  cdleme11l  31003  cdleme11  31004  cdleme12  31005  cdleme14  31007  cdleme15c  31010  cdleme16b  31013  cdleme16d  31015  cdleme17b  31021  cdleme17c  31022  cdleme18c  31027  cdleme18d  31029  cdlemeda  31032  cdlemednpq  31033  cdleme19a  31037  cdleme19c  31039  cdleme20aN  31043  cdleme20bN  31044  cdleme20d  31046  cdleme20f  31048  cdleme20g  31049  cdleme20j  31052  cdleme20l1  31054  cdleme21f  31066  cdleme22aa  31073  cdleme22a  31074  cdleme22cN  31076  cdleme22e  31078  cdleme22f2  31081  cdleme22g  31082  cdleme23b  31084  cdleme23c  31085  cdleme26e  31093  cdleme26fALTN  31096  cdleme26f  31097  cdleme26f2ALTN  31098  cdleme26f2  31099  cdleme28a  31104  cdleme28b  31105  cdleme32b  31176  cdleme32c  31177  cdleme32e  31179  cdleme35h2  31191  cdleme38m  31197  cdleme41sn4aw  31209  cdlemf1  31295  cdlemg1cex  31322  cdlemg2ce  31326  cdlemg4d  31347  cdlemg4f  31349  cdlemg7fvN  31358  cdlemg8a  31361  cdlemg8b  31362  cdlemg8c  31363  cdlemg9a  31366  cdlemg11a  31371  cdlemg11aq  31372  cdlemg10a  31374  cdlemg11b  31376  cdlemg12a  31377  cdlemg12b  31378  cdlemg12d  31380  cdlemg12e  31381  cdlemg12f  31382  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg13  31386  cdlemg14f  31387  cdlemg14g  31388  cdlemg17b  31396  cdlemg17dN  31397  cdlemg17e  31399  cdlemg17h  31402  cdlemg17pq  31406  cdlemg17iqN  31408  cdlemg18b  31413  cdlemg18c  31414  cdlemg18d  31415  cdlemg18  31416  cdlemg19  31418  cdlemg21  31420  cdlemg27a  31426  cdlemg31b0N  31428  cdlemg27b  31430  cdlemg33b0  31435  cdlemg33c0  31436  cdlemg28  31438  cdlemg33a  31440  cdlemg35  31447  cdlemg42  31463  cdlemg44a  31465  cdlemg47  31470  cdlemh2  31550  cdlemh  31551  cdlemj1  31555  cdlemk3  31567  cdlemk5  31570  cdlemki  31575  cdlemksv2  31581  cdlemk7  31582  cdlemk11  31583  cdlemk12  31584  cdlemkole  31587  cdlemk14  31588  cdlemk15  31589  cdlemk16a  31590  cdlemk16  31591  cdlemkj  31597  cdlemkuv2  31601  cdlemk18  31602  cdlemk19  31603  cdlemk7u  31604  cdlemk12u  31606  cdlemkoatnle-2N  31609  cdlemk13-2N  31610  cdlemkole-2N  31611  cdlemk14-2N  31612  cdlemk15-2N  31613  cdlemk16-2N  31614  cdlemk17-2N  31615  cdlemk18-2N  31620  cdlemk19-2N  31621  cdlemk7u-2N  31622  cdlemk11u-2N  31623  cdlemk12u-2N  31624  cdlemk21-2N  31625  cdlemk20-2N  31626  cdlemk22  31627  cdlemk30  31628  cdlemk31  31630  cdlemk32  31631  cdlemk24-3  31637  cdlemkid2  31658  cdlemkfid3N  31659  cdlemk45  31681  cdlemk46  31682  cdlemk47  31683  cdlemk52  31688  cdlemk53a  31689  cdleml1N  31710  cdleml3N  31712  cdlemn7  31938  cdlemn10  31941  dihordlem7  31949  dihord1  31953  dihord2a  31954  dihord10  31958  dihord11c  31959  dihord2pre2  31961  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