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

Theorem simp11 1035
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 1005 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1026 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl11  1080  simpr11  1089  simp111  1134  simp211  1143  simp311  1152  omeulem1  7291  omeu  7294  ackbij1lem16  8663  coprimeprodsq  14722  pythagtriplem14  14741  pythagtrip  14747  mrelatglb  16381  subglsm  17258  lsmpropd  17262  mdetmul  19579  decpmatid  19725  isfil2  20802  filuni  20831  cxple2a  23509  isosctr  23615  brbtwn2  24781  colinearalg  24786  ax5seglem3  24807  numclwwlkovf2ex  25659  gxdi  25869  measres  28883  bayesth  29098  ofscom  30559  btwndiff  30579  ifscgr  30596  brofs2  30629  brifs2  30630  fscgr  30632  btwnconn1lem1  30639  btwnconn1lem2  30640  btwnconn1lem3  30641  btwnconn1lem4  30642  btwnconn1lem5  30643  btwnconn1lem6  30644  btwnconn1lem7  30645  btwnconn1lem8  30646  btwnconn1lem9  30647  btwnconn1lem10  30648  btwnconn1lem11  30649  btwnconn1lem12  30650  seglecgr12im  30662  seglecgr12  30663  ivthALT  30776  eqlkr  32373  lkrshp  32379  lshpkrlem5  32388  cvrval3  32686  4noncolr3  32726  4noncolr2  32727  4noncolr1  32728  athgt  32729  3dimlem2  32732  3dimlem3a  32733  3dimlem4a  32736  3dimlem4  32737  3dimlem4OLDN  32738  3dim2  32741  1cvratex  32746  hlatexch4  32754  ps-2b  32755  3atlem1  32756  3atlem2  32757  3atlem4  32759  3atlem5  32760  3atlem6  32761  llnnleat  32786  2atm  32800  ps-2c  32801  llnmlplnN  32812  lplnnlelln  32816  2atmat  32834  2llnjN  32840  lvoli2  32854  lvolnlelln  32857  4atlem3b  32871  4atlem9  32876  4atlem10a  32877  4atlem10  32879  4atlem11a  32880  4atlem11b  32881  4atlem12a  32883  4atlem12b  32884  4at  32886  4at2  32887  lplncvrlvol2  32888  2lplnj  32893  dalemswapyz  32929  dath2  33010  lneq2at  33051  2lnat  33057  cdlema1N  33064  cdlemb  33067  paddasslem15  33107  pmodlem1  33119  llnmod2i2  33136  llnexchb2lem  33141  llnexchb2  33142  dalawlem1  33144  dalawlem3  33146  dalawlem4  33147  dalawlem5  33148  dalawlem6  33149  dalawlem7  33150  dalawlem8  33151  dalawlem9  33152  dalawlem10  33153  dalawlem11  33154  dalawlem12  33155  dalawlem13  33156  dalawlem15  33158  dalaw  33159  osumcllem5N  33233  osumcllem6N  33234  osumcllem7N  33235  osumcllem9N  33237  osumcllem10N  33238  osumcllem11N  33239  pl42lem1N  33252  lhpexle3lem  33284  lhpmcvr5N  33300  lhp2atne  33307  lhp2at0ne  33309  4atexlemswapqr  33336  4atexlemex6  33347  ldilco  33389  ltrneq  33422  trlval2  33437  trlnidat  33447  cdlemd2  33473  cdlemd7  33478  cdlemd8  33479  cdleme7aa  33516  cdleme7c  33519  cdleme7d  33520  cdleme7e  33521  cdleme7ga  33522  cdleme7  33523  cdleme11c  33535  cdleme11e  33537  cdleme11l  33543  cdleme11  33544  cdleme14  33547  cdleme15a  33548  cdleme15c  33550  cdleme16b  33553  cdleme16c  33554  cdleme16d  33555  cdleme16e  33556  cdleme16f  33557  cdleme0nex  33564  cdleme18d  33569  cdleme19b  33579  cdleme19d  33581  cdleme19e  33582  cdleme20f  33589  cdleme20i  33592  cdleme20k  33594  cdleme20l1  33595  cdleme20l2  33596  cdleme20l  33597  cdleme20m  33598  cdleme21a  33600  cdleme21b  33601  cdleme21ct  33604  cdleme21d  33605  cdleme21e  33606  cdleme21f  33607  cdleme21h  33609  cdleme22eALTN  33620  cdleme22f2  33622  cdleme22g  33623  cdleme26e  33634  cdleme26eALTN  33636  cdleme26fALTN  33637  cdleme26f  33638  cdleme26f2ALTN  33639  cdleme26f2  33640  cdleme28a  33645  cdleme28b  33646  cdleme28  33648  cdleme29ex  33649  cdleme29c  33651  cdlemefrs29cpre1  33673  cdlemefr29exN  33677  cdlemefr32sn2aw  33679  cdlemefr29bpre0N  33681  cdlemefr29clN  33682  cdlemefr32fvaN  33684  cdlemefr32fva1  33685  cdlemefs32sn1aw  33689  cdleme43fsv1snlem  33695  cdleme41sn3a  33708  cdleme32fva  33712  cdleme32b  33717  cdleme32d  33719  cdleme32e  33720  cdleme32f  33721  cdleme32le  33722  cdleme35a  33723  cdleme35fnpq  33724  cdleme35b  33725  cdleme35c  33726  cdleme35d  33727  cdleme35e  33728  cdleme35f  33729  cdleme36a  33735  cdleme36m  33736  cdleme37m  33737  cdleme39a  33740  cdleme39n  33741  cdleme40m  33742  cdleme40n  33743  cdleme42e  33754  cdleme42f  33755  cdleme42g  33756  cdleme43bN  33765  cdleme43cN  33766  cdleme43dN  33767  cdleme46f2g2  33768  cdleme46f2g1  33769  cdleme17d2  33770  cdleme48b  33778  cdleme4gfv  33782  cdlemeg49le  33786  cdlemeg46c  33788  cdlemeg46fvaw  33791  cdlemeg46nlpq  33792  cdlemeg46frv  33800  cdlemeg46rgv  33803  cdlemeg46req  33804  cdlemeg46gfre  33807  cdleme50trn1  33824  cdleme50trn2a  33825  cdleme50trn2  33826  cdleme  33835  cdlemf  33838  trlord  33844  cdlemg2ce  33867  cdlemg7fvbwN  33882  cdlemg7aN  33900  cdlemg10bALTN  33911  cdlemg10a  33915  cdlemg10  33916  cdlemg12d  33921  cdlemg12f  33923  cdlemg12g  33924  cdlemg12  33925  cdlemg13a  33926  cdlemg13  33927  cdlemg17b  33937  cdlemg17dN  33938  cdlemg17dALTN  33939  cdlemg17e  33940  cdlemg17f  33941  cdlemg17g  33942  cdlemg17h  33943  cdlemg17i  33944  cdlemg17pq  33947  cdlemg17bq  33948  cdlemg17iqN  33949  cdlemg17  33952  cdlemg18d  33956  cdlemg18  33957  cdlemg19a  33958  cdlemg19  33959  cdlemg21  33961  cdlemg27a  33967  cdlemg28a  33968  cdlemg31b0N  33969  cdlemg27b  33971  cdlemg33b0  33976  cdlemg28b  33978  cdlemg28  33979  cdlemg33a  33981  cdlemg33  33986  cdlemg34  33987  cdlemg35  33988  cdlemg36  33989  ltrnco  33994  trlcone  34003  cdlemg44  34008  cdlemg47  34011  cdlemg48  34012  tendococl  34047  tendoplcl  34056  cdlemh1  34090  cdlemi  34095  cdlemj1  34096  cdlemj2  34097  tendocan  34099  cdlemk6  34112  cdlemki  34116  cdlemksat  34121  cdlemksv2  34122  cdlemk7  34123  cdlemk11  34124  cdlemk12  34125  cdlemkoatnle  34126  cdlemkole  34128  cdlemk14  34129  cdlemk15  34130  cdlemk16a  34131  cdlemk16  34132  cdlemk17  34133  cdlemk1u  34134  cdlemk5u  34136  cdlemk6u  34137  cdlemkuat  34141  cdlemk18  34143  cdlemk19  34144  cdlemk12u  34147  cdlemk21N  34148  cdlemk20  34149  cdlemkoatnle-2N  34150  cdlemk13-2N  34151  cdlemkole-2N  34152  cdlemk14-2N  34153  cdlemk15-2N  34154  cdlemk16-2N  34155  cdlemk17-2N  34156  cdlemk18-2N  34161  cdlemk19-2N  34162  cdlemk7u-2N  34163  cdlemk11u-2N  34164  cdlemk12u-2N  34165  cdlemk21-2N  34166  cdlemk20-2N  34167  cdlemk22  34168  cdlemk23-3  34177  cdlemk25-3  34179  cdlemk26b-3  34180  cdlemk27-3  34182  cdlemk28-3  34183  cdlemk33N  34184  cdlemk37  34189  cdlemky  34201  cdlemk11ta  34204  cdlemkid3N  34208  cdlemk11tc  34220  cdlemk11t  34221  cdlemk45  34222  cdlemk46  34223  cdlemk47  34224  cdlemk48  34225  cdlemk49  34226  cdlemk50  34227  cdlemk51  34228  cdlemk52  34229  cdlemk55b  34235  cdlemkyyN  34237  cdlemk55u1  34240  cdlemk55u  34241  cdlemk39u1  34242  cdlemk39u  34243  cdlemk56  34246  cdleml3N  34253  cdleml4N  34254  cdlemm10N  34394  dihord1  34494  dihord2a  34495  dihord2b  34496  dihord10  34499  dihord11c  34500  dihord2pre  34501  dihord4  34534  dihord5apre  34538  dihmeetlem1N  34566  dihglbcpreN  34576  dihjatc1  34587  dihjatc3  34589  dihmeetlem13N  34595  dihmeetlem20N  34602  baerlem3lem2  34986  baerlem5alem2  34987  baerlem5blem2  34988  hdmap14lem11  35157  hdmap14lem12  35158  monotuz  35494  congmul  35522  congsub  35525  rpnnen3lem  35591  wessf1ornlem  37081  lincdifsn  38976
  Copyright terms: Public domain W3C validator