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

Theorem simp13 987
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl13  1032  simpr13  1041  simp113  1086  simp213  1095  simp313  1104  omeu  6579  ackbij1lem16  7857  dvdsgcd  12718  coprimeprodsq  12858  pythagtriplem4  12868  pythagtriplem13  12876  pythagtriplem14  12877  pythagtriplem16  12879  pythagtrip  12883  lsmpropd  14982  isfil2  17547  filuni  17576  ufprim  17600  cxple2a  20042  isosctr  20117  brbtwn2  23943  colinearalg  23948  ax5seg  23976  axcontlem4  24005  ofscom  24040  btwndiff  24060  ifscgr  24077  brofs2  24110  brifs2  24111  fscgr  24113  btwnconn1lem1  24120  btwnconn1lem2  24121  btwnconn1lem3  24122  btwnconn1lem4  24123  btwnconn1lem12  24131  seglecgr12im  24143  seglecgr12  24144  intcont  24954  islimrs3  24992  islimrs4  24993  isibg1a6  25536  ivthALT  25669  mzpsubst  26237  congmul  26465  congsub  26468  islshpcv  28522  eqlkr  28568  lshpsmreu  28578  lshpkrlem5  28583  atlrelat1  28790  cvlcvr1  28808  cvlcvrp  28809  cvlatcvr1  28810  cvlatcvr2  28811  4noncolr3  28921  4noncolr2  28922  4noncolr1  28923  athgt  28924  3dimlem2  28927  3dimlem3a  28928  3dimlem4a  28931  3dimlem4  28932  3dimlem4OLDN  28933  3dim1  28935  3dim2  28936  hlatexch4  28949  ps-2b  28950  3atlem6  28956  llnnleat  28981  2atm  28995  ps-2c  28996  llnmlplnN  29007  2atmat  29029  2llnjN  29035  lvoli2  29049  4atlem3b  29066  4atlem10  29074  4atlem11a  29075  4atlem11b  29076  4atlem12a  29078  4atlem12b  29079  dalemswapyz  29124  lneq2at  29246  2lnat  29252  cdlema1N  29259  cdlemb  29262  pmodlem1  29314  llnmod2i2  29331  dalawlem1  29339  dalawlem3  29341  dalawlem4  29342  dalawlem6  29344  dalawlem9  29347  dalawlem10  29348  dalawlem11  29349  dalawlem12  29350  dalawlem13  29351  dalawlem15  29353  dalaw  29354  pclfinN  29368  osumcllem5N  29428  osumcllem6N  29429  osumcllem7N  29430  osumcllem9N  29432  osumcllem11N  29434  pl42lem1N  29447  lhp2at0  29500  lhp2atne  29502  lhp2at0ne  29504  4atexlem7  29543  ldilco  29584  ltrneq  29617  cdlemd2  29667  cdleme0ex2N  29692  cdleme7aa  29710  cdleme7c  29713  cdleme7d  29714  cdleme7ga  29716  cdleme11c  29729  cdleme11l  29737  cdleme11  29738  cdleme14  29741  cdleme15a  29742  cdleme15c  29744  cdleme16b  29747  cdleme16c  29748  cdleme16d  29749  cdleme16e  29750  cdleme16f  29751  cdleme0nex  29758  cdleme19b  29772  cdleme19d  29774  cdleme19e  29775  cdleme20f  29782  cdleme20k  29787  cdleme20l1  29788  cdleme20l2  29789  cdleme20l  29790  cdleme20m  29791  cdleme21a  29793  cdleme21b  29794  cdleme21c  29795  cdleme21ct  29797  cdleme21d  29798  cdleme21e  29799  cdleme21f  29800  cdleme21i  29803  cdleme22cN  29810  cdleme22eALTN  29813  cdleme25a  29821  cdleme25c  29823  cdleme25dN  29824  cdleme26e  29827  cdleme26ee  29828  cdleme26eALTN  29829  cdleme26f2ALTN  29832  cdleme26f2  29833  cdleme28a  29838  cdleme28b  29839  cdleme28  29841  cdlemefr32sn2aw  29872  cdlemefs32sn1aw  29882  cdleme43fsv1snlem  29888  cdleme41sn3a  29901  cdleme32c  29911  cdleme32e  29913  cdleme32le  29915  cdleme35a  29916  cdleme35b  29918  cdleme35d  29920  cdleme36a  29928  cdleme36m  29929  cdleme39a  29933  cdleme40m  29935  cdleme40n  29936  cdleme43bN  29958  cdleme43dN  29960  cdleme46f2g2  29961  cdleme46f2g1  29962  cdleme4gfv  29975  cdlemeg49le  29979  cdlemeg46c  29981  cdlemeg46fvaw  29984  cdlemeg46nlpq  29985  cdlemeg46gfre  30000  cdleme50trn2  30019  cdlemg2ce  30060  cdlemg2idN  30064  cdlemg7fvbwN  30075  cdlemg10bALTN  30104  cdlemg10a  30108  cdlemg12d  30114  cdlemg12g  30117  cdlemg12  30118  cdlemg13a  30119  cdlemg13  30120  cdlemg17b  30130  cdlemg17dN  30131  cdlemg17dALTN  30132  cdlemg17e  30133  cdlemg17pq  30140  cdlemg17bq  30141  cdlemg18d  30149  cdlemg19a  30151  cdlemg19  30152  cdlemg21  30154  cdlemg27a  30160  cdlemg31b0N  30162  cdlemg27b  30164  cdlemg31c  30167  cdlemg33b0  30169  cdlemg33c0  30170  cdlemg28b  30171  cdlemg33a  30174  cdlemg33  30179  ltrnco  30187  cdlemg44  30201  cdlemg47  30204  tendococl  30240  tendoplcl  30249  cdlemh1  30283  cdlemh2  30284  cdlemh  30285  cdlemi  30288  cdlemk5  30304  cdlemk6  30305  cdlemksel  30313  cdlemksv2  30315  cdlemk7  30316  cdlemk11  30317  cdlemk12  30318  cdlemkole  30321  cdlemk14  30322  cdlemk15  30323  cdlemk16a  30324  cdlemk16  30325  cdlemk1u  30327  cdlemk5u  30329  cdlemk6u  30330  cdlemkuel  30333  cdlemkuv2  30335  cdlemk18  30336  cdlemk19  30337  cdlemk7u  30338  cdlemk11u  30339  cdlemk12u  30340  cdlemk21N  30341  cdlemk20  30342  cdlemkoatnle-2N  30343  cdlemk13-2N  30344  cdlemkole-2N  30345  cdlemk14-2N  30346  cdlemk15-2N  30347  cdlemk16-2N  30348  cdlemk17-2N  30349  cdlemk18-2N  30354  cdlemk19-2N  30355  cdlemk7u-2N  30356  cdlemk11u-2N  30357  cdlemk12u-2N  30358  cdlemk21-2N  30359  cdlemk20-2N  30360  cdlemkuel-3  30366  cdlemkuv2-3N  30367  cdlemk22-3  30369  cdlemk33N  30377  cdlemk47  30417  cdlemk48  30418  cdlemk49  30419  cdlemk50  30420  cdlemk51  30421  cdlemk52  30422  cdlemk53a  30423  cdlemk55b  30428  cdlemkyyN  30430  cdlemk55u1  30433  cdlemk39u1  30435  cdlemk56  30439  dihord1  30687  dihord2a  30688  dihord10  30692  dihord11c  30693  dihord4  30727  dihord5apre  30731  dihglblem2N  30763  dihglbcpreN  30769  dihmeetlem3N  30774  dihjatc1  30780  dihjatc2N  30781  dihjatc3  30782  mapdpglem24  31173  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  hdmap14lem11  31350  hdmap14lem12  31351  hdmapglem7  31401
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