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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
213ad2ant1 977 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935
This theorem is referenced by:  simpl13  1033  simpr13  1042  simp113  1087  simp213  1096  simp313  1105  funtpg  5405  omeu  6725  ackbij1lem16  8008  dvdsgcd  12930  coprimeprodsq  13070  pythagtriplem4  13080  pythagtriplem13  13088  pythagtriplem14  13089  pythagtriplem16  13091  pythagtrip  13095  lsmpropd  15196  isfil2  17764  filuni  17793  ufprim  17817  cxple2a  20268  isosctr  20343  measres  24039  bayesth  24145  brbtwn2  25275  colinearalg  25280  ax5seg  25308  axcontlem4  25337  ofscom  25372  btwndiff  25392  ifscgr  25409  brofs2  25442  brifs2  25443  fscgr  25445  btwnconn1lem1  25452  btwnconn1lem2  25453  btwnconn1lem3  25454  btwnconn1lem4  25455  btwnconn1lem12  25463  seglecgr12im  25475  seglecgr12  25476  ivthALT  25765  mzpsubst  26332  congmul  26560  congsub  26563  islshpcv  29314  eqlkr  29360  lshpsmreu  29370  lshpkrlem5  29375  atlrelat1  29582  cvlcvr1  29600  cvlcvrp  29601  cvlatcvr1  29602  cvlatcvr2  29603  4noncolr3  29713  4noncolr2  29714  4noncolr1  29715  athgt  29716  3dimlem2  29719  3dimlem3a  29720  3dimlem4a  29723  3dimlem4  29724  3dimlem4OLDN  29725  3dim1  29727  3dim2  29728  hlatexch4  29741  ps-2b  29742  3atlem6  29748  llnnleat  29773  2atm  29787  ps-2c  29788  llnmlplnN  29799  2atmat  29821  2llnjN  29827  lvoli2  29841  4atlem3b  29858  4atlem10  29866  4atlem11a  29867  4atlem11b  29868  4atlem12a  29870  4atlem12b  29871  dalemswapyz  29916  lneq2at  30038  2lnat  30044  cdlema1N  30051  cdlemb  30054  pmodlem1  30106  llnmod2i2  30123  dalawlem1  30131  dalawlem3  30133  dalawlem4  30134  dalawlem6  30136  dalawlem9  30139  dalawlem10  30140  dalawlem11  30141  dalawlem12  30142  dalawlem13  30143  dalawlem15  30145  dalaw  30146  pclfinN  30160  osumcllem5N  30220  osumcllem6N  30221  osumcllem7N  30222  osumcllem9N  30224  osumcllem11N  30226  pl42lem1N  30239  lhp2at0  30292  lhp2atne  30294  lhp2at0ne  30296  4atexlem7  30335  ldilco  30376  ltrneq  30409  cdlemd2  30459  cdleme0ex2N  30484  cdleme7aa  30502  cdleme7c  30505  cdleme7d  30506  cdleme7ga  30508  cdleme11c  30521  cdleme11l  30529  cdleme11  30530  cdleme14  30533  cdleme15a  30534  cdleme15c  30536  cdleme16b  30539  cdleme16c  30540  cdleme16d  30541  cdleme16e  30542  cdleme16f  30543  cdleme0nex  30550  cdleme19b  30564  cdleme19d  30566  cdleme19e  30567  cdleme20f  30574  cdleme20k  30579  cdleme20l1  30580  cdleme20l2  30581  cdleme20l  30582  cdleme20m  30583  cdleme21a  30585  cdleme21b  30586  cdleme21c  30587  cdleme21ct  30589  cdleme21d  30590  cdleme21e  30591  cdleme21f  30592  cdleme21i  30595  cdleme22cN  30602  cdleme22eALTN  30605  cdleme25a  30613  cdleme25c  30615  cdleme25dN  30616  cdleme26e  30619  cdleme26ee  30620  cdleme26eALTN  30621  cdleme26f2ALTN  30624  cdleme26f2  30625  cdleme28a  30630  cdleme28b  30631  cdleme28  30633  cdlemefr32sn2aw  30664  cdlemefs32sn1aw  30674  cdleme43fsv1snlem  30680  cdleme41sn3a  30693  cdleme32c  30703  cdleme32e  30705  cdleme32le  30707  cdleme35a  30708  cdleme35b  30710  cdleme35d  30712  cdleme36a  30720  cdleme36m  30721  cdleme39a  30725  cdleme40m  30727  cdleme40n  30728  cdleme43bN  30750  cdleme43dN  30752  cdleme46f2g2  30753  cdleme46f2g1  30754  cdleme4gfv  30767  cdlemeg49le  30771  cdlemeg46c  30773  cdlemeg46fvaw  30776  cdlemeg46nlpq  30777  cdlemeg46gfre  30792  cdleme50trn2  30811  cdlemg2ce  30852  cdlemg2idN  30856  cdlemg7fvbwN  30867  cdlemg10bALTN  30896  cdlemg10a  30900  cdlemg12d  30906  cdlemg12g  30909  cdlemg12  30910  cdlemg13a  30911  cdlemg13  30912  cdlemg17b  30922  cdlemg17dN  30923  cdlemg17dALTN  30924  cdlemg17e  30925  cdlemg17pq  30932  cdlemg17bq  30933  cdlemg18d  30941  cdlemg19a  30943  cdlemg19  30944  cdlemg21  30946  cdlemg27a  30952  cdlemg31b0N  30954  cdlemg27b  30956  cdlemg31c  30959  cdlemg33b0  30961  cdlemg33c0  30962  cdlemg28b  30963  cdlemg33a  30966  cdlemg33  30971  ltrnco  30979  cdlemg44  30993  cdlemg47  30996  tendococl  31032  tendoplcl  31041  cdlemh1  31075  cdlemh2  31076  cdlemh  31077  cdlemi  31080  cdlemk5  31096  cdlemk6  31097  cdlemksel  31105  cdlemksv2  31107  cdlemk7  31108  cdlemk11  31109  cdlemk12  31110  cdlemkole  31113  cdlemk14  31114  cdlemk15  31115  cdlemk16a  31116  cdlemk16  31117  cdlemk1u  31119  cdlemk5u  31121  cdlemk6u  31122  cdlemkuel  31125  cdlemkuv2  31127  cdlemk18  31128  cdlemk19  31129  cdlemk7u  31130  cdlemk11u  31131  cdlemk12u  31132  cdlemk21N  31133  cdlemk20  31134  cdlemkoatnle-2N  31135  cdlemk13-2N  31136  cdlemkole-2N  31137  cdlemk14-2N  31138  cdlemk15-2N  31139  cdlemk16-2N  31140  cdlemk17-2N  31141  cdlemk18-2N  31146  cdlemk19-2N  31147  cdlemk7u-2N  31148  cdlemk11u-2N  31149  cdlemk12u-2N  31150  cdlemk21-2N  31151  cdlemk20-2N  31152  cdlemkuel-3  31158  cdlemkuv2-3N  31159  cdlemk22-3  31161  cdlemk33N  31169  cdlemk47  31209  cdlemk48  31210  cdlemk49  31211  cdlemk50  31212  cdlemk51  31213  cdlemk52  31214  cdlemk53a  31215  cdlemk55b  31220  cdlemkyyN  31222  cdlemk55u1  31225  cdlemk39u1  31227  cdlemk56  31231  dihord1  31479  dihord2a  31480  dihord10  31484  dihord11c  31485  dihord4  31519  dihord5apre  31523  dihglblem2N  31555  dihglbcpreN  31561  dihmeetlem3N  31566  dihjatc1  31572  dihjatc2N  31573  dihjatc3  31574  mapdpglem24  31965  baerlem3lem2  31971  baerlem5alem2  31972  baerlem5blem2  31973  hdmap14lem11  32142  hdmap14lem12  32143  hdmapglem7  32193
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 937
  Copyright terms: Public domain W3C validator