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  7294  omeu  7297  ackbij1lem16  8672  coprimeprodsq  14758  pythagtriplem14  14777  pythagtrip  14783  mrelatglb  16429  subglsm  17322  lsmpropd  17326  mdetmul  19646  decpmatid  19792  isfil2  20869  filuni  20898  cxple2a  23642  isosctr  23748  brbtwn2  24933  colinearalg  24938  ax5seglem3  24959  numclwwlkovf2ex  25812  gxdi  26022  measres  29052  bayesth  29280  ofscom  30779  btwndiff  30799  ifscgr  30816  brofs2  30849  brifs2  30850  fscgr  30852  btwnconn1lem1  30859  btwnconn1lem2  30860  btwnconn1lem3  30861  btwnconn1lem4  30862  btwnconn1lem5  30863  btwnconn1lem6  30864  btwnconn1lem7  30865  btwnconn1lem8  30866  btwnconn1lem9  30867  btwnconn1lem10  30868  btwnconn1lem11  30869  btwnconn1lem12  30870  seglecgr12im  30882  seglecgr12  30883  ivthALT  30996  eqlkr  32634  lkrshp  32640  lshpkrlem5  32649  cvrval3  32947  4noncolr3  32987  4noncolr2  32988  4noncolr1  32989  athgt  32990  3dimlem2  32993  3dimlem3a  32994  3dimlem4a  32997  3dimlem4  32998  3dimlem4OLDN  32999  3dim2  33002  1cvratex  33007  hlatexch4  33015  ps-2b  33016  3atlem1  33017  3atlem2  33018  3atlem4  33020  3atlem5  33021  3atlem6  33022  llnnleat  33047  2atm  33061  ps-2c  33062  llnmlplnN  33073  lplnnlelln  33077  2atmat  33095  2llnjN  33101  lvoli2  33115  lvolnlelln  33118  4atlem3b  33132  4atlem9  33137  4atlem10a  33138  4atlem10  33140  4atlem11a  33141  4atlem11b  33142  4atlem12a  33144  4atlem12b  33145  4at  33147  4at2  33148  lplncvrlvol2  33149  2lplnj  33154  dalemswapyz  33190  dath2  33271  lneq2at  33312  2lnat  33318  cdlema1N  33325  cdlemb  33328  paddasslem15  33368  pmodlem1  33380  llnmod2i2  33397  llnexchb2lem  33402  llnexchb2  33403  dalawlem1  33405  dalawlem3  33407  dalawlem4  33408  dalawlem5  33409  dalawlem6  33410  dalawlem7  33411  dalawlem8  33412  dalawlem9  33413  dalawlem10  33414  dalawlem11  33415  dalawlem12  33416  dalawlem13  33417  dalawlem15  33419  dalaw  33420  osumcllem5N  33494  osumcllem6N  33495  osumcllem7N  33496  osumcllem9N  33498  osumcllem10N  33499  osumcllem11N  33500  pl42lem1N  33513  lhpexle3lem  33545  lhpmcvr5N  33561  lhp2atne  33568  lhp2at0ne  33570  4atexlemswapqr  33597  4atexlemex6  33608  ldilco  33650  ltrneq  33683  trlval2  33698  trlnidat  33708  cdlemd2  33734  cdlemd7  33739  cdlemd8  33740  cdleme7aa  33777  cdleme7c  33780  cdleme7d  33781  cdleme7e  33782  cdleme7ga  33783  cdleme7  33784  cdleme11c  33796  cdleme11e  33798  cdleme11l  33804  cdleme11  33805  cdleme14  33808  cdleme15a  33809  cdleme15c  33811  cdleme16b  33814  cdleme16c  33815  cdleme16d  33816  cdleme16e  33817  cdleme16f  33818  cdleme0nex  33825  cdleme18d  33830  cdleme19b  33840  cdleme19d  33842  cdleme19e  33843  cdleme20f  33850  cdleme20i  33853  cdleme20k  33855  cdleme20l1  33856  cdleme20l2  33857  cdleme20l  33858  cdleme20m  33859  cdleme21a  33861  cdleme21b  33862  cdleme21ct  33865  cdleme21d  33866  cdleme21e  33867  cdleme21f  33868  cdleme21h  33870  cdleme22eALTN  33881  cdleme22f2  33883  cdleme22g  33884  cdleme26e  33895  cdleme26eALTN  33897  cdleme26fALTN  33898  cdleme26f  33899  cdleme26f2ALTN  33900  cdleme26f2  33901  cdleme28a  33906  cdleme28b  33907  cdleme28  33909  cdleme29ex  33910  cdleme29c  33912  cdlemefrs29cpre1  33934  cdlemefr29exN  33938  cdlemefr32sn2aw  33940  cdlemefr29bpre0N  33942  cdlemefr29clN  33943  cdlemefr32fvaN  33945  cdlemefr32fva1  33946  cdlemefs32sn1aw  33950  cdleme43fsv1snlem  33956  cdleme41sn3a  33969  cdleme32fva  33973  cdleme32b  33978  cdleme32d  33980  cdleme32e  33981  cdleme32f  33982  cdleme32le  33983  cdleme35a  33984  cdleme35fnpq  33985  cdleme35b  33986  cdleme35c  33987  cdleme35d  33988  cdleme35e  33989  cdleme35f  33990  cdleme36a  33996  cdleme36m  33997  cdleme37m  33998  cdleme39a  34001  cdleme39n  34002  cdleme40m  34003  cdleme40n  34004  cdleme42e  34015  cdleme42f  34016  cdleme42g  34017  cdleme43bN  34026  cdleme43cN  34027  cdleme43dN  34028  cdleme46f2g2  34029  cdleme46f2g1  34030  cdleme17d2  34031  cdleme48b  34039  cdleme4gfv  34043  cdlemeg49le  34047  cdlemeg46c  34049  cdlemeg46fvaw  34052  cdlemeg46nlpq  34053  cdlemeg46frv  34061  cdlemeg46rgv  34064  cdlemeg46req  34065  cdlemeg46gfre  34068  cdleme50trn1  34085  cdleme50trn2a  34086  cdleme50trn2  34087  cdleme  34096  cdlemf  34099  trlord  34105  cdlemg2ce  34128  cdlemg7fvbwN  34143  cdlemg7aN  34161  cdlemg10bALTN  34172  cdlemg10a  34176  cdlemg10  34177  cdlemg12d  34182  cdlemg12f  34184  cdlemg12g  34185  cdlemg12  34186  cdlemg13a  34187  cdlemg13  34188  cdlemg17b  34198  cdlemg17dN  34199  cdlemg17dALTN  34200  cdlemg17e  34201  cdlemg17f  34202  cdlemg17g  34203  cdlemg17h  34204  cdlemg17i  34205  cdlemg17pq  34208  cdlemg17bq  34209  cdlemg17iqN  34210  cdlemg17  34213  cdlemg18d  34217  cdlemg18  34218  cdlemg19a  34219  cdlemg19  34220  cdlemg21  34222  cdlemg27a  34228  cdlemg28a  34229  cdlemg31b0N  34230  cdlemg27b  34232  cdlemg33b0  34237  cdlemg28b  34239  cdlemg28  34240  cdlemg33a  34242  cdlemg33  34247  cdlemg34  34248  cdlemg35  34249  cdlemg36  34250  ltrnco  34255  trlcone  34264  cdlemg44  34269  cdlemg47  34272  cdlemg48  34273  tendococl  34308  tendoplcl  34317  cdlemh1  34351  cdlemi  34356  cdlemj1  34357  cdlemj2  34358  tendocan  34360  cdlemk6  34373  cdlemki  34377  cdlemksat  34382  cdlemksv2  34383  cdlemk7  34384  cdlemk11  34385  cdlemk12  34386  cdlemkoatnle  34387  cdlemkole  34389  cdlemk14  34390  cdlemk15  34391  cdlemk16a  34392  cdlemk16  34393  cdlemk17  34394  cdlemk1u  34395  cdlemk5u  34397  cdlemk6u  34398  cdlemkuat  34402  cdlemk18  34404  cdlemk19  34405  cdlemk12u  34408  cdlemk21N  34409  cdlemk20  34410  cdlemkoatnle-2N  34411  cdlemk13-2N  34412  cdlemkole-2N  34413  cdlemk14-2N  34414  cdlemk15-2N  34415  cdlemk16-2N  34416  cdlemk17-2N  34417  cdlemk18-2N  34422  cdlemk19-2N  34423  cdlemk7u-2N  34424  cdlemk11u-2N  34425  cdlemk12u-2N  34426  cdlemk21-2N  34427  cdlemk20-2N  34428  cdlemk22  34429  cdlemk23-3  34438  cdlemk25-3  34440  cdlemk26b-3  34441  cdlemk27-3  34443  cdlemk28-3  34444  cdlemk33N  34445  cdlemk37  34450  cdlemky  34462  cdlemk11ta  34465  cdlemkid3N  34469  cdlemk11tc  34481  cdlemk11t  34482  cdlemk45  34483  cdlemk46  34484  cdlemk47  34485  cdlemk48  34486  cdlemk49  34487  cdlemk50  34488  cdlemk51  34489  cdlemk52  34490  cdlemk55b  34496  cdlemkyyN  34498  cdlemk55u1  34501  cdlemk55u  34502  cdlemk39u1  34503  cdlemk39u  34504  cdlemk56  34507  cdleml3N  34514  cdleml4N  34515  cdlemm10N  34655  dihord1  34755  dihord2a  34756  dihord2b  34757  dihord10  34760  dihord11c  34761  dihord2pre  34762  dihord4  34795  dihord5apre  34799  dihmeetlem1N  34827  dihglbcpreN  34837  dihjatc1  34848  dihjatc3  34850  dihmeetlem13N  34856  dihmeetlem20N  34863  baerlem3lem2  35247  baerlem5alem2  35248  baerlem5blem2  35249  hdmap14lem11  35418  hdmap14lem12  35419  monotuz  35759  congmul  35787  congsub  35790  rpnnen3lem  35856  wessf1ornlem  37420  lincdifsn  39839
  Copyright terms: Public domain W3C validator