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

Theorem simp33 993
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 957 . 2  |-  ( ( ch  /\  th  /\  ta )  ->  ta )
213ad2ant3 978 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  th  /\  ta ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl33  1038  simpr33  1047  simp133  1092  simp233  1101  simp333  1110  smogt  6468  bitsfzo  12717  logexprlim  20570  iocinioc2  23341  ax5seg  25125  cgrtr  25174  cgrtr3  25176  ofscom  25189  segconeq  25192  btwnxfr  25238  colinearxfr  25257  fscgr  25262  btwnconn1lem1  25269  btwnconn1lem2  25270  btwnconn1lem5  25273  btwnconn1lem6  25274  btwnconn1lem8  25276  btwnconn1lem9  25277  btwnconn1lem10  25278  btwnconn1lem11  25279  btwnconn1lem12  25280  brsegle2  25291  seglecgr12im  25292  seglecgr12  25293  segletr  25296  outsideofeq  25312  fmuldfeq  27036  bnj966  28721  lshpkrlem5  29356  lshpkrlem6  29357  atbtwnexOLDN  29688  atbtwnex  29689  4noncolr3  29694  3dimlem3a  29701  3dimlem4a  29704  3dim1  29708  3dim2  29709  1cvrat  29717  2atjlej  29720  hlatexch4  29722  ps-2b  29723  2atm  29768  ps-2c  29769  lvolex3N  29779  2atmat  29802  lvolnlelpln  29826  4atlem10  29847  4atlem11b  29849  4atlem11  29850  4at  29854  4at2  29855  2lplnja  29860  2lplnj  29861  dalemclccjdd  29929  paddasslem5  30065  paddasslem15  30075  pmodlem1  30087  dalawlem1  30112  dalawlem3  30114  dalawlem4  30115  dalawlem5  30116  dalawlem6  30117  dalawlem7  30118  dalawlem8  30119  dalawlem9  30120  dalawlem11  30122  dalawlem12  30123  dalawlem15  30126  osumcllem5N  30201  osumcllem6N  30202  lhpexle3lem  30252  lhpmcvr4N  30267  lhpmcvr6N  30269  4atexlemex6  30315  4atex2  30318  4atex2-0bOLDN  30320  4atex3  30322  ltrn11at  30388  cdlemd3  30441  cdleme7aa  30483  cdleme7b  30485  cdleme7c  30486  cdleme7d  30487  cdleme7ga  30489  cdleme16aN  30500  cdleme11dN  30503  cdleme11e  30504  cdleme11l  30510  cdleme11  30511  cdleme12  30512  cdleme14  30514  cdleme15c  30517  cdleme16b  30520  cdleme16d  30522  cdleme17b  30528  cdleme17c  30529  cdleme18c  30534  cdleme18d  30536  cdlemeda  30539  cdlemednpq  30540  cdleme19a  30544  cdleme19c  30546  cdleme20aN  30550  cdleme20bN  30551  cdleme20d  30553  cdleme20f  30555  cdleme20g  30556  cdleme20j  30559  cdleme20l1  30561  cdleme21f  30573  cdleme22aa  30580  cdleme22a  30581  cdleme22cN  30583  cdleme22e  30585  cdleme22f2  30588  cdleme22g  30589  cdleme23b  30591  cdleme23c  30592  cdleme26e  30600  cdleme26fALTN  30603  cdleme26f  30604  cdleme26f2ALTN  30605  cdleme26f2  30606  cdleme28a  30611  cdleme28b  30612  cdleme32b  30683  cdleme32c  30684  cdleme32e  30686  cdleme35h2  30698  cdleme38m  30704  cdleme41sn4aw  30716  cdlemf1  30802  cdlemg1cex  30829  cdlemg2ce  30833  cdlemg4d  30854  cdlemg4f  30856  cdlemg7fvN  30865  cdlemg8a  30868  cdlemg8b  30869  cdlemg8c  30870  cdlemg9a  30873  cdlemg11a  30878  cdlemg11aq  30879  cdlemg10a  30881  cdlemg11b  30883  cdlemg12a  30884  cdlemg12b  30885  cdlemg12d  30887  cdlemg12e  30888  cdlemg12f  30889  cdlemg12g  30890  cdlemg12  30891  cdlemg13a  30892  cdlemg13  30893  cdlemg14f  30894  cdlemg14g  30895  cdlemg17b  30903  cdlemg17dN  30904  cdlemg17e  30906  cdlemg17h  30909  cdlemg17pq  30913  cdlemg17iqN  30915  cdlemg18b  30920  cdlemg18c  30921  cdlemg18d  30922  cdlemg18  30923  cdlemg19  30925  cdlemg21  30927  cdlemg27a  30933  cdlemg31b0N  30935  cdlemg27b  30937  cdlemg33b0  30942  cdlemg33c0  30943  cdlemg28  30945  cdlemg33a  30947  cdlemg35  30954  cdlemg42  30970  cdlemg44a  30972  cdlemg47  30977  cdlemh2  31057  cdlemh  31058  cdlemj1  31062  cdlemk3  31074  cdlemk5  31077  cdlemki  31082  cdlemksv2  31088  cdlemk7  31089  cdlemk11  31090  cdlemk12  31091  cdlemkole  31094  cdlemk14  31095  cdlemk15  31096  cdlemk16a  31097  cdlemk16  31098  cdlemkj  31104  cdlemkuv2  31108  cdlemk18  31109  cdlemk19  31110  cdlemk7u  31111  cdlemk12u  31113  cdlemkoatnle-2N  31116  cdlemk13-2N  31117  cdlemkole-2N  31118  cdlemk14-2N  31119  cdlemk15-2N  31120  cdlemk16-2N  31121  cdlemk17-2N  31122  cdlemk18-2N  31127  cdlemk19-2N  31128  cdlemk7u-2N  31129  cdlemk11u-2N  31130  cdlemk12u-2N  31131  cdlemk21-2N  31132  cdlemk20-2N  31133  cdlemk22  31134  cdlemk30  31135  cdlemk31  31137  cdlemk32  31138  cdlemk24-3  31144  cdlemkid2  31165  cdlemkfid3N  31166  cdlemk45  31188  cdlemk46  31189  cdlemk47  31190  cdlemk52  31195  cdlemk53a  31196  cdleml1N  31217  cdleml3N  31219  cdlemn7  31445  cdlemn10  31448  dihordlem7  31456  dihord1  31460  dihord2a  31461  dihord10  31465  dihord11c  31466  dihord2pre2  31468  hlhilphllem  32204
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