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

Theorem simp11 1024
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 994 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  simpl11  1069  simpr11  1078  simp111  1123  simp211  1132  simp311  1141  omeulem1  7223  omeu  7226  ackbij1lem16  8606  coprimeprodsq  14420  pythagtriplem14  14439  pythagtrip  14445  mrelatglb  16016  subglsm  16893  lsmpropd  16897  mdetmul  19295  decpmatid  19441  isfil2  20526  filuni  20555  cxple2a  23251  isosctr  23355  brbtwn2  24413  colinearalg  24418  ax5seglem3  24439  numclwwlkovf2ex  25291  gxdi  25499  measres  28433  bayesth  28645  ofscom  29888  btwndiff  29908  ifscgr  29925  brofs2  29958  brifs2  29959  fscgr  29961  btwnconn1lem1  29968  btwnconn1lem2  29969  btwnconn1lem3  29970  btwnconn1lem4  29971  btwnconn1lem5  29972  btwnconn1lem6  29973  btwnconn1lem7  29974  btwnconn1lem8  29975  btwnconn1lem9  29976  btwnconn1lem10  29977  btwnconn1lem11  29978  btwnconn1lem12  29979  seglecgr12im  29991  seglecgr12  29992  ivthALT  30396  monotuz  31119  congmul  31147  congsub  31150  rpnnen3lem  31215  lincdifsn  33298  eqlkr  35240  lkrshp  35246  lshpkrlem5  35255  cvrval3  35553  4noncolr3  35593  4noncolr2  35594  4noncolr1  35595  athgt  35596  3dimlem2  35599  3dimlem3a  35600  3dimlem4a  35603  3dimlem4  35604  3dimlem4OLDN  35605  3dim2  35608  1cvratex  35613  hlatexch4  35621  ps-2b  35622  3atlem1  35623  3atlem2  35624  3atlem4  35626  3atlem5  35627  3atlem6  35628  llnnleat  35653  2atm  35667  ps-2c  35668  llnmlplnN  35679  lplnnlelln  35683  2atmat  35701  2llnjN  35707  lvoli2  35721  lvolnlelln  35724  4atlem3b  35738  4atlem9  35743  4atlem10a  35744  4atlem10  35746  4atlem11a  35747  4atlem11b  35748  4atlem12a  35750  4atlem12b  35751  4at  35753  4at2  35754  lplncvrlvol2  35755  2lplnj  35760  dalemswapyz  35796  dath2  35877  lneq2at  35918  2lnat  35924  cdlema1N  35931  cdlemb  35934  paddasslem15  35974  pmodlem1  35986  llnmod2i2  36003  llnexchb2lem  36008  llnexchb2  36009  dalawlem1  36011  dalawlem3  36013  dalawlem4  36014  dalawlem5  36015  dalawlem6  36016  dalawlem7  36017  dalawlem8  36018  dalawlem9  36019  dalawlem10  36020  dalawlem11  36021  dalawlem12  36022  dalawlem13  36023  dalawlem15  36025  dalaw  36026  osumcllem5N  36100  osumcllem6N  36101  osumcllem7N  36102  osumcllem9N  36104  osumcllem10N  36105  osumcllem11N  36106  pl42lem1N  36119  lhpexle3lem  36151  lhpmcvr5N  36167  lhp2atne  36174  lhp2at0ne  36176  4atexlemswapqr  36203  4atexlemex6  36214  ldilco  36256  ltrneq  36289  trlval2  36304  trlnidat  36314  cdlemd2  36340  cdlemd7  36345  cdlemd8  36346  cdleme7aa  36383  cdleme7c  36386  cdleme7d  36387  cdleme7e  36388  cdleme7ga  36389  cdleme7  36390  cdleme11c  36402  cdleme11e  36404  cdleme11l  36410  cdleme11  36411  cdleme14  36414  cdleme15a  36415  cdleme15c  36417  cdleme16b  36420  cdleme16c  36421  cdleme16d  36422  cdleme16e  36423  cdleme16f  36424  cdleme0nex  36431  cdleme18d  36436  cdleme19b  36446  cdleme19d  36448  cdleme19e  36449  cdleme20f  36456  cdleme20i  36459  cdleme20k  36461  cdleme20l1  36462  cdleme20l2  36463  cdleme20l  36464  cdleme20m  36465  cdleme21a  36467  cdleme21b  36468  cdleme21ct  36471  cdleme21d  36472  cdleme21e  36473  cdleme21f  36474  cdleme21h  36476  cdleme22eALTN  36487  cdleme22f2  36489  cdleme22g  36490  cdleme26e  36501  cdleme26eALTN  36503  cdleme26fALTN  36504  cdleme26f  36505  cdleme26f2ALTN  36506  cdleme26f2  36507  cdleme28a  36512  cdleme28b  36513  cdleme28  36515  cdleme29ex  36516  cdleme29c  36518  cdlemefrs29cpre1  36540  cdlemefr29exN  36544  cdlemefr32sn2aw  36546  cdlemefr29bpre0N  36548  cdlemefr29clN  36549  cdlemefr32fvaN  36551  cdlemefr32fva1  36552  cdlemefs32sn1aw  36556  cdleme43fsv1snlem  36562  cdleme41sn3a  36575  cdleme32fva  36579  cdleme32b  36584  cdleme32d  36586  cdleme32e  36587  cdleme32f  36588  cdleme32le  36589  cdleme35a  36590  cdleme35fnpq  36591  cdleme35b  36592  cdleme35c  36593  cdleme35d  36594  cdleme35e  36595  cdleme35f  36596  cdleme36a  36602  cdleme36m  36603  cdleme37m  36604  cdleme39a  36607  cdleme39n  36608  cdleme40m  36609  cdleme40n  36610  cdleme42e  36621  cdleme42f  36622  cdleme42g  36623  cdleme43bN  36632  cdleme43cN  36633  cdleme43dN  36634  cdleme46f2g2  36635  cdleme46f2g1  36636  cdleme17d2  36637  cdleme48b  36645  cdleme4gfv  36649  cdlemeg49le  36653  cdlemeg46c  36655  cdlemeg46fvaw  36658  cdlemeg46nlpq  36659  cdlemeg46frv  36667  cdlemeg46rgv  36670  cdlemeg46req  36671  cdlemeg46gfre  36674  cdleme50trn1  36691  cdleme50trn2a  36692  cdleme50trn2  36693  cdleme  36702  cdlemf  36705  trlord  36711  cdlemg2ce  36734  cdlemg7fvbwN  36749  cdlemg7aN  36767  cdlemg10bALTN  36778  cdlemg10a  36782  cdlemg10  36783  cdlemg12d  36788  cdlemg12f  36790  cdlemg12g  36791  cdlemg12  36792  cdlemg13a  36793  cdlemg13  36794  cdlemg17b  36804  cdlemg17dN  36805  cdlemg17dALTN  36806  cdlemg17e  36807  cdlemg17f  36808  cdlemg17g  36809  cdlemg17h  36810  cdlemg17i  36811  cdlemg17pq  36814  cdlemg17bq  36815  cdlemg17iqN  36816  cdlemg17  36819  cdlemg18d  36823  cdlemg18  36824  cdlemg19a  36825  cdlemg19  36826  cdlemg21  36828  cdlemg27a  36834  cdlemg28a  36835  cdlemg31b0N  36836  cdlemg27b  36838  cdlemg33b0  36843  cdlemg28b  36845  cdlemg28  36846  cdlemg33a  36848  cdlemg33  36853  cdlemg34  36854  cdlemg35  36855  cdlemg36  36856  ltrnco  36861  trlcone  36870  cdlemg44  36875  cdlemg47  36878  cdlemg48  36879  tendococl  36914  tendoplcl  36923  cdlemh1  36957  cdlemi  36962  cdlemj1  36963  cdlemj2  36964  tendocan  36966  cdlemk6  36979  cdlemki  36983  cdlemksat  36988  cdlemksv2  36989  cdlemk7  36990  cdlemk11  36991  cdlemk12  36992  cdlemkoatnle  36993  cdlemkole  36995  cdlemk14  36996  cdlemk15  36997  cdlemk16a  36998  cdlemk16  36999  cdlemk17  37000  cdlemk1u  37001  cdlemk5u  37003  cdlemk6u  37004  cdlemkuat  37008  cdlemk18  37010  cdlemk19  37011  cdlemk12u  37014  cdlemk21N  37015  cdlemk20  37016  cdlemkoatnle-2N  37017  cdlemk13-2N  37018  cdlemkole-2N  37019  cdlemk14-2N  37020  cdlemk15-2N  37021  cdlemk16-2N  37022  cdlemk17-2N  37023  cdlemk18-2N  37028  cdlemk19-2N  37029  cdlemk7u-2N  37030  cdlemk11u-2N  37031  cdlemk12u-2N  37032  cdlemk21-2N  37033  cdlemk20-2N  37034  cdlemk22  37035  cdlemk23-3  37044  cdlemk25-3  37046  cdlemk26b-3  37047  cdlemk27-3  37049  cdlemk28-3  37050  cdlemk33N  37051  cdlemk37  37056  cdlemky  37068  cdlemk11ta  37071  cdlemkid3N  37075  cdlemk11tc  37087  cdlemk11t  37088  cdlemk45  37089  cdlemk46  37090  cdlemk47  37091  cdlemk48  37092  cdlemk49  37093  cdlemk50  37094  cdlemk51  37095  cdlemk52  37096  cdlemk55b  37102  cdlemkyyN  37104  cdlemk55u1  37107  cdlemk55u  37108  cdlemk39u1  37109  cdlemk39u  37110  cdlemk56  37113  cdleml3N  37120  cdleml4N  37121  cdlemm10N  37261  dihord1  37361  dihord2a  37362  dihord2b  37363  dihord10  37366  dihord11c  37367  dihord2pre  37368  dihord4  37401  dihord5apre  37405  dihmeetlem1N  37433  dihglbcpreN  37443  dihjatc1  37454  dihjatc3  37456  dihmeetlem13N  37462  dihmeetlem20N  37469  baerlem3lem2  37853  baerlem5alem2  37854  baerlem5blem2  37855  hdmap14lem11  38024  hdmap14lem12  38025
  Copyright terms: Public domain W3C validator