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

Theorem simp11 1039
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 1009 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1030 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 986
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 190  df-an 377  df-3an 988
This theorem is referenced by:  simpl11  1084  simpr11  1093  simp111  1138  simp211  1147  simp311  1156  funcnvqp  5620  omeulem1  7270  omeu  7273  ackbij1lem16  8652  coprimeprodsq  14770  pythagtriplem14  14789  pythagtrip  14795  mrelatglb  16441  subglsm  17334  lsmpropd  17338  mdetmul  19659  decpmatid  19805  isfil2  20882  filuni  20911  cxple2a  23656  isosctr  23762  brbtwn2  24947  colinearalg  24952  ax5seglem3  24973  numclwwlkovf2ex  25826  gxdi  26036  measres  29051  bayesth  29278  ofscom  30780  btwndiff  30800  ifscgr  30817  brofs2  30850  brifs2  30851  fscgr  30853  btwnconn1lem1  30860  btwnconn1lem2  30861  btwnconn1lem3  30862  btwnconn1lem4  30863  btwnconn1lem5  30864  btwnconn1lem6  30865  btwnconn1lem7  30866  btwnconn1lem8  30867  btwnconn1lem9  30868  btwnconn1lem10  30869  btwnconn1lem11  30870  btwnconn1lem12  30871  seglecgr12im  30883  seglecgr12  30884  ivthALT  30997  eqlkr  32667  lkrshp  32673  lshpkrlem5  32682  cvrval3  32980  4noncolr3  33020  4noncolr2  33021  4noncolr1  33022  athgt  33023  3dimlem2  33026  3dimlem3a  33027  3dimlem4a  33030  3dimlem4  33031  3dimlem4OLDN  33032  3dim2  33035  1cvratex  33040  hlatexch4  33048  ps-2b  33049  3atlem1  33050  3atlem2  33051  3atlem4  33053  3atlem5  33054  3atlem6  33055  llnnleat  33080  2atm  33094  ps-2c  33095  llnmlplnN  33106  lplnnlelln  33110  2atmat  33128  2llnjN  33134  lvoli2  33148  lvolnlelln  33151  4atlem3b  33165  4atlem9  33170  4atlem10a  33171  4atlem10  33173  4atlem11a  33174  4atlem11b  33175  4atlem12a  33177  4atlem12b  33178  4at  33180  4at2  33181  lplncvrlvol2  33182  2lplnj  33187  dalemswapyz  33223  dath2  33304  lneq2at  33345  2lnat  33351  cdlema1N  33358  cdlemb  33361  paddasslem15  33401  pmodlem1  33413  llnmod2i2  33430  llnexchb2lem  33435  llnexchb2  33436  dalawlem1  33438  dalawlem3  33440  dalawlem4  33441  dalawlem5  33442  dalawlem6  33443  dalawlem7  33444  dalawlem8  33445  dalawlem9  33446  dalawlem10  33447  dalawlem11  33448  dalawlem12  33449  dalawlem13  33450  dalawlem15  33452  dalaw  33453  osumcllem5N  33527  osumcllem6N  33528  osumcllem7N  33529  osumcllem9N  33531  osumcllem10N  33532  osumcllem11N  33533  pl42lem1N  33546  lhpexle3lem  33578  lhpmcvr5N  33594  lhp2atne  33601  lhp2at0ne  33603  4atexlemswapqr  33630  4atexlemex6  33641  ldilco  33683  ltrneq  33716  trlval2  33731  trlnidat  33741  cdlemd2  33767  cdlemd7  33772  cdlemd8  33773  cdleme7aa  33810  cdleme7c  33813  cdleme7d  33814  cdleme7e  33815  cdleme7ga  33816  cdleme7  33817  cdleme11c  33829  cdleme11e  33831  cdleme11l  33837  cdleme11  33838  cdleme14  33841  cdleme15a  33842  cdleme15c  33844  cdleme16b  33847  cdleme16c  33848  cdleme16d  33849  cdleme16e  33850  cdleme16f  33851  cdleme0nex  33858  cdleme18d  33863  cdleme19b  33873  cdleme19d  33875  cdleme19e  33876  cdleme20f  33883  cdleme20i  33886  cdleme20k  33888  cdleme20l1  33889  cdleme20l2  33890  cdleme20l  33891  cdleme20m  33892  cdleme21a  33894  cdleme21b  33895  cdleme21ct  33898  cdleme21d  33899  cdleme21e  33900  cdleme21f  33901  cdleme21h  33903  cdleme22eALTN  33914  cdleme22f2  33916  cdleme22g  33917  cdleme26e  33928  cdleme26eALTN  33930  cdleme26fALTN  33931  cdleme26f  33932  cdleme26f2ALTN  33933  cdleme26f2  33934  cdleme28a  33939  cdleme28b  33940  cdleme28  33942  cdleme29ex  33943  cdleme29c  33945  cdlemefrs29cpre1  33967  cdlemefr29exN  33971  cdlemefr32sn2aw  33973  cdlemefr29bpre0N  33975  cdlemefr29clN  33976  cdlemefr32fvaN  33978  cdlemefr32fva1  33979  cdlemefs32sn1aw  33983  cdleme43fsv1snlem  33989  cdleme41sn3a  34002  cdleme32fva  34006  cdleme32b  34011  cdleme32d  34013  cdleme32e  34014  cdleme32f  34015  cdleme32le  34016  cdleme35a  34017  cdleme35fnpq  34018  cdleme35b  34019  cdleme35c  34020  cdleme35d  34021  cdleme35e  34022  cdleme35f  34023  cdleme36a  34029  cdleme36m  34030  cdleme37m  34031  cdleme39a  34034  cdleme39n  34035  cdleme40m  34036  cdleme40n  34037  cdleme42e  34048  cdleme42f  34049  cdleme42g  34050  cdleme43bN  34059  cdleme43cN  34060  cdleme43dN  34061  cdleme46f2g2  34062  cdleme46f2g1  34063  cdleme17d2  34064  cdleme48b  34072  cdleme4gfv  34076  cdlemeg49le  34080  cdlemeg46c  34082  cdlemeg46fvaw  34085  cdlemeg46nlpq  34086  cdlemeg46frv  34094  cdlemeg46rgv  34097  cdlemeg46req  34098  cdlemeg46gfre  34101  cdleme50trn1  34118  cdleme50trn2a  34119  cdleme50trn2  34120  cdleme  34129  cdlemf  34132  trlord  34138  cdlemg2ce  34161  cdlemg7fvbwN  34176  cdlemg7aN  34194  cdlemg10bALTN  34205  cdlemg10a  34209  cdlemg10  34210  cdlemg12d  34215  cdlemg12f  34217  cdlemg12g  34218  cdlemg12  34219  cdlemg13a  34220  cdlemg13  34221  cdlemg17b  34231  cdlemg17dN  34232  cdlemg17dALTN  34233  cdlemg17e  34234  cdlemg17f  34235  cdlemg17g  34236  cdlemg17h  34237  cdlemg17i  34238  cdlemg17pq  34241  cdlemg17bq  34242  cdlemg17iqN  34243  cdlemg17  34246  cdlemg18d  34250  cdlemg18  34251  cdlemg19a  34252  cdlemg19  34253  cdlemg21  34255  cdlemg27a  34261  cdlemg28a  34262  cdlemg31b0N  34263  cdlemg27b  34265  cdlemg33b0  34270  cdlemg28b  34272  cdlemg28  34273  cdlemg33a  34275  cdlemg33  34280  cdlemg34  34281  cdlemg35  34282  cdlemg36  34283  ltrnco  34288  trlcone  34297  cdlemg44  34302  cdlemg47  34305  cdlemg48  34306  tendococl  34341  tendoplcl  34350  cdlemh1  34384  cdlemi  34389  cdlemj1  34390  cdlemj2  34391  tendocan  34393  cdlemk6  34406  cdlemki  34410  cdlemksat  34415  cdlemksv2  34416  cdlemk7  34417  cdlemk11  34418  cdlemk12  34419  cdlemkoatnle  34420  cdlemkole  34422  cdlemk14  34423  cdlemk15  34424  cdlemk16a  34425  cdlemk16  34426  cdlemk17  34427  cdlemk1u  34428  cdlemk5u  34430  cdlemk6u  34431  cdlemkuat  34435  cdlemk18  34437  cdlemk19  34438  cdlemk12u  34441  cdlemk21N  34442  cdlemk20  34443  cdlemkoatnle-2N  34444  cdlemk13-2N  34445  cdlemkole-2N  34446  cdlemk14-2N  34447  cdlemk15-2N  34448  cdlemk16-2N  34449  cdlemk17-2N  34450  cdlemk18-2N  34455  cdlemk19-2N  34456  cdlemk7u-2N  34457  cdlemk11u-2N  34458  cdlemk12u-2N  34459  cdlemk21-2N  34460  cdlemk20-2N  34461  cdlemk22  34462  cdlemk23-3  34471  cdlemk25-3  34473  cdlemk26b-3  34474  cdlemk27-3  34476  cdlemk28-3  34477  cdlemk33N  34478  cdlemk37  34483  cdlemky  34495  cdlemk11ta  34498  cdlemkid3N  34502  cdlemk11tc  34514  cdlemk11t  34515  cdlemk45  34516  cdlemk46  34517  cdlemk47  34518  cdlemk48  34519  cdlemk49  34520  cdlemk50  34521  cdlemk51  34522  cdlemk52  34523  cdlemk55b  34529  cdlemkyyN  34531  cdlemk55u1  34534  cdlemk55u  34535  cdlemk39u1  34536  cdlemk39u  34537  cdlemk56  34540  cdleml3N  34547  cdleml4N  34548  cdlemm10N  34688  dihord1  34788  dihord2a  34789  dihord2b  34790  dihord10  34793  dihord11c  34794  dihord2pre  34795  dihord4  34828  dihord5apre  34832  dihmeetlem1N  34860  dihglbcpreN  34870  dihjatc1  34881  dihjatc3  34883  dihmeetlem13N  34889  dihmeetlem20N  34896  baerlem3lem2  35280  baerlem5alem2  35281  baerlem5blem2  35282  hdmap14lem11  35451  hdmap14lem12  35452  monotuz  35791  congmul  35819  congsub  35822  rpnnen3lem  35888  wessf1ornlem  37469  infleinf  37627  lincdifsn  40542
  Copyright terms: Public domain W3C validator