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

Theorem simp11 987
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl11  1032  simpr11  1041  simp111  1086  simp211  1095  simp311  1104  omeulem1  6817  omeu  6820  ackbij1lem16  8107  coprimeprodsq  13175  pythagtriplem14  13194  pythagtrip  13200  mrelatglb  14602  subglsm  15297  lsmpropd  15301  isfil2  17880  filuni  17909  cxple2a  20582  isosctr  20657  gxdi  21876  measres  24568  bayesth  24689  brbtwn2  25836  colinearalg  25841  ax5seglem3  25862  ofscom  25933  btwndiff  25953  ifscgr  25970  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem5  26017  btwnconn1lem6  26018  btwnconn1lem7  26019  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem10  26022  btwnconn1lem11  26023  btwnconn1lem12  26024  seglecgr12im  26036  seglecgr12  26037  ivthALT  26329  monotuz  26995  congmul  27023  congsub  27026  rpnnen3lem  27093  eqlkr  29834  lkrshp  29840  lshpkrlem5  29849  cvrval3  30147  4noncolr3  30187  4noncolr2  30188  4noncolr1  30189  athgt  30190  3dimlem2  30193  3dimlem3a  30194  3dimlem4a  30197  3dimlem4  30198  3dimlem4OLDN  30199  3dim2  30202  1cvratex  30207  hlatexch4  30215  ps-2b  30216  3atlem1  30217  3atlem2  30218  3atlem4  30220  3atlem5  30221  3atlem6  30222  llnnleat  30247  2atm  30261  ps-2c  30262  llnmlplnN  30273  lplnnlelln  30277  2atmat  30295  2llnjN  30301  lvoli2  30315  lvolnlelln  30318  4atlem3b  30332  4atlem9  30337  4atlem10a  30338  4atlem10  30340  4atlem11a  30341  4atlem11b  30342  4atlem12a  30344  4atlem12b  30345  4at  30347  4at2  30348  lplncvrlvol2  30349  2lplnj  30354  dalemswapyz  30390  dath2  30471  lneq2at  30512  2lnat  30518  cdlema1N  30525  cdlemb  30528  paddasslem15  30568  pmodlem1  30580  llnmod2i2  30597  llnexchb2lem  30602  llnexchb2  30603  dalawlem1  30605  dalawlem3  30607  dalawlem4  30608  dalawlem5  30609  dalawlem6  30610  dalawlem7  30611  dalawlem8  30612  dalawlem9  30613  dalawlem10  30614  dalawlem11  30615  dalawlem12  30616  dalawlem13  30617  dalawlem15  30619  dalaw  30620  osumcllem5N  30694  osumcllem6N  30695  osumcllem7N  30696  osumcllem9N  30698  osumcllem10N  30699  osumcllem11N  30700  pl42lem1N  30713  lhpexle3lem  30745  lhpmcvr5N  30761  lhp2atne  30768  lhp2at0ne  30770  4atexlemswapqr  30797  4atexlemex6  30808  ldilco  30850  ltrneq  30883  trlval2  30897  trlnidat  30907  cdlemd2  30933  cdlemd7  30938  cdlemd8  30939  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme11c  30995  cdleme11e  30997  cdleme11l  31003  cdleme11  31004  cdleme14  31007  cdleme15a  31008  cdleme15c  31010  cdleme16b  31013  cdleme16c  31014  cdleme16d  31015  cdleme16e  31016  cdleme16f  31017  cdleme0nex  31024  cdleme18d  31029  cdleme19b  31038  cdleme19d  31040  cdleme19e  31041  cdleme20f  31048  cdleme20i  31051  cdleme20k  31053  cdleme20l1  31054  cdleme20l2  31055  cdleme20l  31056  cdleme20m  31057  cdleme21a  31059  cdleme21b  31060  cdleme21ct  31063  cdleme21d  31064  cdleme21e  31065  cdleme21f  31066  cdleme21h  31068  cdleme22eALTN  31079  cdleme22f2  31081  cdleme22g  31082  cdleme26e  31093  cdleme26eALTN  31095  cdleme26fALTN  31096  cdleme26f  31097  cdleme26f2ALTN  31098  cdleme26f2  31099  cdleme28a  31104  cdleme28b  31105  cdleme28  31107  cdleme29ex  31108  cdleme29c  31110  cdlemefrs29cpre1  31132  cdlemefr29exN  31136  cdlemefr32sn2aw  31138  cdlemefr29bpre0N  31140  cdlemefr29clN  31141  cdlemefr32fvaN  31143  cdlemefr32fva1  31144  cdlemefs32sn1aw  31148  cdleme43fsv1snlem  31154  cdleme41sn3a  31167  cdleme32fva  31171  cdleme32b  31176  cdleme32d  31178  cdleme32e  31179  cdleme32f  31180  cdleme32le  31181  cdleme35a  31182  cdleme35fnpq  31183  cdleme35b  31184  cdleme35c  31185  cdleme35d  31186  cdleme35e  31187  cdleme35f  31188  cdleme36a  31194  cdleme36m  31195  cdleme37m  31196  cdleme39a  31199  cdleme39n  31200  cdleme40m  31201  cdleme40n  31202  cdleme42e  31213  cdleme42f  31214  cdleme42g  31215  cdleme43bN  31224  cdleme43cN  31225  cdleme43dN  31226  cdleme46f2g2  31227  cdleme46f2g1  31228  cdleme17d2  31229  cdleme48b  31237  cdleme4gfv  31241  cdlemeg49le  31245  cdlemeg46c  31247  cdlemeg46fvaw  31250  cdlemeg46nlpq  31251  cdlemeg46frv  31259  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemeg46gfre  31266  cdleme50trn1  31283  cdleme50trn2a  31284  cdleme50trn2  31285  cdleme  31294  cdlemf  31297  trlord  31303  cdlemg2ce  31326  cdlemg7fvbwN  31341  cdlemg7aN  31359  cdlemg10bALTN  31370  cdlemg10a  31374  cdlemg10  31375  cdlemg12d  31380  cdlemg12f  31382  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg13  31386  cdlemg17b  31396  cdlemg17dN  31397  cdlemg17dALTN  31398  cdlemg17e  31399  cdlemg17f  31400  cdlemg17g  31401  cdlemg17h  31402  cdlemg17i  31403  cdlemg17pq  31406  cdlemg17bq  31407  cdlemg17iqN  31408  cdlemg17  31411  cdlemg18d  31415  cdlemg18  31416  cdlemg19a  31417  cdlemg19  31418  cdlemg21  31420  cdlemg27a  31426  cdlemg28a  31427  cdlemg31b0N  31428  cdlemg27b  31430  cdlemg33b0  31435  cdlemg28b  31437  cdlemg28  31438  cdlemg33a  31440  cdlemg33  31445  cdlemg34  31446  cdlemg35  31447  cdlemg36  31448  ltrnco  31453  trlcone  31462  cdlemg44  31467  cdlemg47  31470  cdlemg48  31471  tendococl  31506  tendoplcl  31515  cdlemh1  31549  cdlemi  31554  cdlemj1  31555  cdlemj2  31556  tendocan  31558  cdlemk6  31571  cdlemki  31575  cdlemksat  31580  cdlemksv2  31581  cdlemk7  31582  cdlemk11  31583  cdlemk12  31584  cdlemkoatnle  31585  cdlemkole  31587  cdlemk14  31588  cdlemk15  31589  cdlemk16a  31590  cdlemk16  31591  cdlemk17  31592  cdlemk1u  31593  cdlemk5u  31595  cdlemk6u  31596  cdlemkuat  31600  cdlemk18  31602  cdlemk19  31603  cdlemk12u  31606  cdlemk21N  31607  cdlemk20  31608  cdlemkoatnle-2N  31609  cdlemk13-2N  31610  cdlemkole-2N  31611  cdlemk14-2N  31612  cdlemk15-2N  31613  cdlemk16-2N  31614  cdlemk17-2N  31615  cdlemk18-2N  31620  cdlemk19-2N  31621  cdlemk7u-2N  31622  cdlemk11u-2N  31623  cdlemk12u-2N  31624  cdlemk21-2N  31625  cdlemk20-2N  31626  cdlemk22  31627  cdlemk23-3  31636  cdlemk25-3  31638  cdlemk26b-3  31639  cdlemk27-3  31641  cdlemk28-3  31642  cdlemk33N  31643  cdlemk37  31648  cdlemky  31660  cdlemk11ta  31663  cdlemkid3N  31667  cdlemk11tc  31679  cdlemk11t  31680  cdlemk45  31681  cdlemk46  31682  cdlemk47  31683  cdlemk48  31684  cdlemk49  31685  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  cdlemk55b  31694  cdlemkyyN  31696  cdlemk55u1  31699  cdlemk55u  31700  cdlemk39u1  31701  cdlemk39u  31702  cdlemk56  31705  cdleml3N  31712  cdleml4N  31713  cdlemm10N  31853  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord10  31958  dihord11c  31959  dihord2pre  31960  dihord4  31993  dihord5apre  31997  dihmeetlem1N  32025  dihglbcpreN  32035  dihjatc1  32046  dihjatc3  32048  dihmeetlem13N  32054  dihmeetlem20N  32061  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  hdmap14lem11  32616  hdmap14lem12  32617
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator