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  6580  omeu  6583  ackbij1lem16  7861  coprimeprodsq  12862  pythagtriplem14  12881  pythagtrip  12887  mrelatglb  14287  subglsm  14982  lsmpropd  14986  isfil2  17551  filuni  17580  cxple2a  20046  isosctr  20121  gxdi  20963  measres  23549  bayesth  23642  brbtwn2  24533  colinearalg  24538  ax5seglem3  24559  ofscom  24630  btwndiff  24650  ifscgr  24667  brofs2  24700  brifs2  24701  fscgr  24703  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn1lem12  24721  seglecgr12im  24733  seglecgr12  24734  svli2  25484  islimrs3  25581  islimrs4  25582  isibg1a6  26125  ivthALT  26258  monotuz  27026  congmul  27054  congsub  27057  rpnnen3lem  27124  eqlkr  29289  lkrshp  29295  lshpkrlem5  29304  cvrval3  29602  4noncolr3  29642  4noncolr2  29643  4noncolr1  29644  athgt  29645  3dimlem2  29648  3dimlem3a  29649  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  3dim2  29657  1cvratex  29662  hlatexch4  29670  ps-2b  29671  3atlem1  29672  3atlem2  29673  3atlem4  29675  3atlem5  29676  3atlem6  29677  llnnleat  29702  2atm  29716  ps-2c  29717  llnmlplnN  29728  lplnnlelln  29732  2atmat  29750  2llnjN  29756  lvoli2  29770  lvolnlelln  29773  4atlem3b  29787  4atlem9  29792  4atlem10a  29793  4atlem10  29795  4atlem11a  29796  4atlem11b  29797  4atlem12a  29799  4atlem12b  29800  4at  29802  4at2  29803  lplncvrlvol2  29804  2lplnj  29809  dalemswapyz  29845  dath2  29926  lneq2at  29967  2lnat  29973  cdlema1N  29980  cdlemb  29983  paddasslem15  30023  pmodlem1  30035  llnmod2i2  30052  llnexchb2lem  30057  llnexchb2  30058  dalawlem1  30060  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem10  30069  dalawlem11  30070  dalawlem12  30071  dalawlem13  30072  dalawlem15  30074  dalaw  30075  osumcllem5N  30149  osumcllem6N  30150  osumcllem7N  30151  osumcllem9N  30153  osumcllem10N  30154  osumcllem11N  30155  pl42lem1N  30168  lhpexle3lem  30200  lhpmcvr5N  30216  lhp2atne  30223  lhp2at0ne  30225  4atexlemswapqr  30252  4atexlemex6  30263  ldilco  30305  ltrneq  30338  trlval2  30352  trlnidat  30362  cdlemd2  30388  cdlemd7  30393  cdlemd8  30394  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme11c  30450  cdleme11e  30452  cdleme11l  30458  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme0nex  30479  cdleme18d  30484  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20f  30503  cdleme20i  30506  cdleme20k  30508  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21a  30514  cdleme21b  30515  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme21f  30521  cdleme21h  30523  cdleme22eALTN  30534  cdleme22f2  30536  cdleme22g  30537  cdleme26e  30548  cdleme26eALTN  30550  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme28a  30559  cdleme28b  30560  cdleme28  30562  cdleme29ex  30563  cdleme29c  30565  cdlemefrs29cpre1  30587  cdlemefr29exN  30591  cdlemefr32sn2aw  30593  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32fva  30626  cdleme32b  30631  cdleme32d  30633  cdleme32e  30634  cdleme32f  30635  cdleme32le  30636  cdleme35a  30637  cdleme35fnpq  30638  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme35f  30643  cdleme36a  30649  cdleme36m  30650  cdleme37m  30651  cdleme39a  30654  cdleme39n  30655  cdleme40m  30656  cdleme40n  30657  cdleme42e  30668  cdleme42f  30669  cdleme42g  30670  cdleme43bN  30679  cdleme43cN  30680  cdleme43dN  30681  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme17d2  30684  cdleme48b  30692  cdleme4gfv  30696  cdlemeg49le  30700  cdlemeg46c  30702  cdlemeg46fvaw  30705  cdlemeg46nlpq  30706  cdlemeg46frv  30714  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfre  30721  cdleme50trn1  30738  cdleme50trn2a  30739  cdleme50trn2  30740  cdleme  30749  cdlemf  30752  trlord  30758  cdlemg2ce  30781  cdlemg7fvbwN  30796  cdlemg7aN  30814  cdlemg10bALTN  30825  cdlemg10a  30829  cdlemg10  30830  cdlemg12d  30835  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg17b  30851  cdlemg17dN  30852  cdlemg17dALTN  30853  cdlemg17e  30854  cdlemg17f  30855  cdlemg17g  30856  cdlemg17h  30857  cdlemg17i  30858  cdlemg17pq  30861  cdlemg17bq  30862  cdlemg17iqN  30863  cdlemg17  30866  cdlemg18d  30870  cdlemg18  30871  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg28a  30882  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg33b0  30890  cdlemg28b  30892  cdlemg28  30893  cdlemg33a  30895  cdlemg33  30900  cdlemg34  30901  cdlemg35  30902  cdlemg36  30903  ltrnco  30908  trlcone  30917  cdlemg44  30922  cdlemg47  30925  cdlemg48  30926  tendococl  30961  tendoplcl  30970  cdlemh1  31004  cdlemi  31009  cdlemj1  31010  cdlemj2  31011  tendocan  31013  cdlemk6  31026  cdlemki  31030  cdlemksat  31035  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkoatnle  31040  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  cdlemk17  31047  cdlemk1u  31048  cdlemk5u  31050  cdlemk6u  31051  cdlemkuat  31055  cdlemk18  31057  cdlemk19  31058  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk21-2N  31080  cdlemk20-2N  31081  cdlemk22  31082  cdlemk23-3  31091  cdlemk25-3  31093  cdlemk26b-3  31094  cdlemk27-3  31096  cdlemk28-3  31097  cdlemk33N  31098  cdlemk37  31103  cdlemky  31115  cdlemk11ta  31118  cdlemkid3N  31122  cdlemk11tc  31134  cdlemk11t  31135  cdlemk45  31136  cdlemk46  31137  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk55b  31149  cdlemkyyN  31151  cdlemk55u1  31154  cdlemk55u  31155  cdlemk39u1  31156  cdlemk39u  31157  cdlemk56  31160  cdleml3N  31167  cdleml4N  31168  cdlemm10N  31308  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord10  31413  dihord11c  31414  dihord2pre  31415  dihord4  31448  dihord5apre  31452  dihmeetlem1N  31480  dihglbcpreN  31490  dihjatc1  31501  dihjatc3  31503  dihmeetlem13N  31509  dihmeetlem20N  31516  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmap14lem11  32071  hdmap14lem12  32072
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