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

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

Proof of Theorem simp11
StepHypRef Expression
1 simp1 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl11  1030  simpr11  1039  simp111  1084  simp211  1093  simp311  1102  omeulem1  6576  omeu  6579  ackbij1lem16  7857  coprimeprodsq  12858  pythagtriplem14  12877  pythagtrip  12883  mrelatglb  14283  subglsm  14978  lsmpropd  14982  isfil2  17547  filuni  17576  cxple2a  20042  isosctr  20117  gxdi  20957  brbtwn2  23943  colinearalg  23948  ax5seglem3  23969  ofscom  24040  btwndiff  24060  ifscgr  24077  brofs2  24110  brifs2  24111  fscgr  24113  btwnconn1lem1  24120  btwnconn1lem2  24121  btwnconn1lem3  24122  btwnconn1lem4  24123  btwnconn1lem5  24124  btwnconn1lem6  24125  btwnconn1lem7  24126  btwnconn1lem8  24127  btwnconn1lem9  24128  btwnconn1lem10  24129  btwnconn1lem11  24130  btwnconn1lem12  24131  seglecgr12im  24143  seglecgr12  24144  svli2  24895  islimrs3  24992  islimrs4  24993  isibg1a6  25536  ivthALT  25669  monotuz  26437  congmul  26465  congsub  26468  rpnnen3lem  26535  eqlkr  28568  lkrshp  28574  lshpkrlem5  28583  cvrval3  28881  4noncolr3  28921  4noncolr2  28922  4noncolr1  28923  athgt  28924  3dimlem2  28927  3dimlem3a  28928  3dimlem4a  28931  3dimlem4  28932  3dimlem4OLDN  28933  3dim2  28936  1cvratex  28941  hlatexch4  28949  ps-2b  28950  3atlem1  28951  3atlem2  28952  3atlem4  28954  3atlem5  28955  3atlem6  28956  llnnleat  28981  2atm  28995  ps-2c  28996  llnmlplnN  29007  lplnnlelln  29011  2atmat  29029  2llnjN  29035  lvoli2  29049  lvolnlelln  29052  4atlem3b  29066  4atlem9  29071  4atlem10a  29072  4atlem10  29074  4atlem11a  29075  4atlem11b  29076  4atlem12a  29078  4atlem12b  29079  4at  29081  4at2  29082  lplncvrlvol2  29083  2lplnj  29088  dalemswapyz  29124  dath2  29205  lneq2at  29246  2lnat  29252  cdlema1N  29259  cdlemb  29262  paddasslem15  29302  pmodlem1  29314  llnmod2i2  29331  llnexchb2lem  29336  llnexchb2  29337  dalawlem1  29339  dalawlem3  29341  dalawlem4  29342  dalawlem5  29343  dalawlem6  29344  dalawlem7  29345  dalawlem8  29346  dalawlem9  29347  dalawlem10  29348  dalawlem11  29349  dalawlem12  29350  dalawlem13  29351  dalawlem15  29353  dalaw  29354  osumcllem5N  29428  osumcllem6N  29429  osumcllem7N  29430  osumcllem9N  29432  osumcllem10N  29433  osumcllem11N  29434  pl42lem1N  29447  lhpexle3lem  29479  lhpmcvr5N  29495  lhp2atne  29502  lhp2at0ne  29504  4atexlemswapqr  29531  4atexlemex6  29542  ldilco  29584  ltrneq  29617  trlval2  29631  trlnidat  29641  cdlemd2  29667  cdlemd7  29672  cdlemd8  29673  cdleme7aa  29710  cdleme7c  29713  cdleme7d  29714  cdleme7e  29715  cdleme7ga  29716  cdleme7  29717  cdleme11c  29729  cdleme11e  29731  cdleme11l  29737  cdleme11  29738  cdleme14  29741  cdleme15a  29742  cdleme15c  29744  cdleme16b  29747  cdleme16c  29748  cdleme16d  29749  cdleme16e  29750  cdleme16f  29751  cdleme0nex  29758  cdleme18d  29763  cdleme19b  29772  cdleme19d  29774  cdleme19e  29775  cdleme20f  29782  cdleme20i  29785  cdleme20k  29787  cdleme20l1  29788  cdleme20l2  29789  cdleme20l  29790  cdleme20m  29791  cdleme21a  29793  cdleme21b  29794  cdleme21ct  29797  cdleme21d  29798  cdleme21e  29799  cdleme21f  29800  cdleme21h  29802  cdleme22eALTN  29813  cdleme22f2  29815  cdleme22g  29816  cdleme26e  29827  cdleme26eALTN  29829  cdleme26fALTN  29830  cdleme26f  29831  cdleme26f2ALTN  29832  cdleme26f2  29833  cdleme28a  29838  cdleme28b  29839  cdleme28  29841  cdleme29ex  29842  cdleme29c  29844  cdlemefrs29cpre1  29866  cdlemefr29exN  29870  cdlemefr32sn2aw  29872  cdlemefr29bpre0N  29874  cdlemefr29clN  29875  cdlemefr32fvaN  29877  cdlemefr32fva1  29878  cdlemefs32sn1aw  29882  cdleme43fsv1snlem  29888  cdleme41sn3a  29901  cdleme32fva  29905  cdleme32b  29910  cdleme32d  29912  cdleme32e  29913  cdleme32f  29914  cdleme32le  29915  cdleme35a  29916  cdleme35fnpq  29917  cdleme35b  29918  cdleme35c  29919  cdleme35d  29920  cdleme35e  29921  cdleme35f  29922  cdleme36a  29928  cdleme36m  29929  cdleme37m  29930  cdleme39a  29933  cdleme39n  29934  cdleme40m  29935  cdleme40n  29936  cdleme42e  29947  cdleme42f  29948  cdleme42g  29949  cdleme43bN  29958  cdleme43cN  29959  cdleme43dN  29960  cdleme46f2g2  29961  cdleme46f2g1  29962  cdleme17d2  29963  cdleme48b  29971  cdleme4gfv  29975  cdlemeg49le  29979  cdlemeg46c  29981  cdlemeg46fvaw  29984  cdlemeg46nlpq  29985  cdlemeg46frv  29993  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemeg46gfre  30000  cdleme50trn1  30017  cdleme50trn2a  30018  cdleme50trn2  30019  cdleme  30028  cdlemf  30031  trlord  30037  cdlemg2ce  30060  cdlemg7fvbwN  30075  cdlemg7aN  30093  cdlemg10bALTN  30104  cdlemg10a  30108  cdlemg10  30109  cdlemg12d  30114  cdlemg12f  30116  cdlemg12g  30117  cdlemg12  30118  cdlemg13a  30119  cdlemg13  30120  cdlemg17b  30130  cdlemg17dN  30131  cdlemg17dALTN  30132  cdlemg17e  30133  cdlemg17f  30134  cdlemg17g  30135  cdlemg17h  30136  cdlemg17i  30137  cdlemg17pq  30140  cdlemg17bq  30141  cdlemg17iqN  30142  cdlemg17  30145  cdlemg18d  30149  cdlemg18  30150  cdlemg19a  30151  cdlemg19  30152  cdlemg21  30154  cdlemg27a  30160  cdlemg28a  30161  cdlemg31b0N  30162  cdlemg27b  30164  cdlemg33b0  30169  cdlemg28b  30171  cdlemg28  30172  cdlemg33a  30174  cdlemg33  30179  cdlemg34  30180  cdlemg35  30181  cdlemg36  30182  ltrnco  30187  trlcone  30196  cdlemg44  30201  cdlemg47  30204  cdlemg48  30205  tendococl  30240  tendoplcl  30249  cdlemh1  30283  cdlemi  30288  cdlemj1  30289  cdlemj2  30290  tendocan  30292  cdlemk6  30305  cdlemki  30309  cdlemksat  30314  cdlemksv2  30315  cdlemk7  30316  cdlemk11  30317  cdlemk12  30318  cdlemkoatnle  30319  cdlemkole  30321  cdlemk14  30322  cdlemk15  30323  cdlemk16a  30324  cdlemk16  30325  cdlemk17  30326  cdlemk1u  30327  cdlemk5u  30329  cdlemk6u  30330  cdlemkuat  30334  cdlemk18  30336  cdlemk19  30337  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  cdlemk22  30361  cdlemk23-3  30370  cdlemk25-3  30372  cdlemk26b-3  30373  cdlemk27-3  30375  cdlemk28-3  30376  cdlemk33N  30377  cdlemk37  30382  cdlemky  30394  cdlemk11ta  30397  cdlemkid3N  30401  cdlemk11tc  30413  cdlemk11t  30414  cdlemk45  30415  cdlemk46  30416  cdlemk47  30417  cdlemk48  30418  cdlemk49  30419  cdlemk50  30420  cdlemk51  30421  cdlemk52  30422  cdlemk55b  30428  cdlemkyyN  30430  cdlemk55u1  30433  cdlemk55u  30434  cdlemk39u1  30435  cdlemk39u  30436  cdlemk56  30439  cdleml3N  30446  cdleml4N  30447  cdlemm10N  30587  dihord1  30687  dihord2a  30688  dihord2b  30689  dihord10  30692  dihord11c  30693  dihord2pre  30694  dihord4  30727  dihord5apre  30731  dihmeetlem1N  30759  dihglbcpreN  30769  dihjatc1  30780  dihjatc3  30782  dihmeetlem13N  30788  dihmeetlem20N  30795  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  hdmap14lem11  31350  hdmap14lem12  31351
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