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

Theorem simp11 985
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 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl11  1030  simpr11  1039  simp111  1084  simp211  1093  simp311  1102  omeulem1  6596  omeu  6599  ackbij1lem16  7877  coprimeprodsq  12878  pythagtriplem14  12897  pythagtrip  12903  mrelatglb  14303  subglsm  14998  lsmpropd  15002  isfil2  17567  filuni  17596  cxple2a  20062  isosctr  20137  gxdi  20979  measres  23564  bayesth  23657  brbtwn2  24605  colinearalg  24610  ax5seglem3  24631  ofscom  24702  btwndiff  24722  ifscgr  24739  brofs2  24772  brifs2  24773  fscgr  24775  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn1lem12  24793  seglecgr12im  24805  seglecgr12  24806  svli2  25587  islimrs3  25684  islimrs4  25685  isibg1a6  26228  ivthALT  26361  monotuz  27129  congmul  27157  congsub  27160  rpnnen3lem  27227  eqlkr  29911  lkrshp  29917  lshpkrlem5  29926  cvrval3  30224  4noncolr3  30264  4noncolr2  30265  4noncolr1  30266  athgt  30267  3dimlem2  30270  3dimlem3a  30271  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  3dim2  30279  1cvratex  30284  hlatexch4  30292  ps-2b  30293  3atlem1  30294  3atlem2  30295  3atlem4  30297  3atlem5  30298  3atlem6  30299  llnnleat  30324  2atm  30338  ps-2c  30339  llnmlplnN  30350  lplnnlelln  30354  2atmat  30372  2llnjN  30378  lvoli2  30392  lvolnlelln  30395  4atlem3b  30409  4atlem9  30414  4atlem10a  30415  4atlem10  30417  4atlem11a  30418  4atlem11b  30419  4atlem12a  30421  4atlem12b  30422  4at  30424  4at2  30425  lplncvrlvol2  30426  2lplnj  30431  dalemswapyz  30467  dath2  30548  lneq2at  30589  2lnat  30595  cdlema1N  30602  cdlemb  30605  paddasslem15  30645  pmodlem1  30657  llnmod2i2  30674  llnexchb2lem  30679  llnexchb2  30680  dalawlem1  30682  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem10  30691  dalawlem11  30692  dalawlem12  30693  dalawlem13  30694  dalawlem15  30696  dalaw  30697  osumcllem5N  30771  osumcllem6N  30772  osumcllem7N  30773  osumcllem9N  30775  osumcllem10N  30776  osumcllem11N  30777  pl42lem1N  30790  lhpexle3lem  30822  lhpmcvr5N  30838  lhp2atne  30845  lhp2at0ne  30847  4atexlemswapqr  30874  4atexlemex6  30885  ldilco  30927  ltrneq  30960  trlval2  30974  trlnidat  30984  cdlemd2  31010  cdlemd7  31015  cdlemd8  31016  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11c  31072  cdleme11e  31074  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme0nex  31101  cdleme18d  31106  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20f  31125  cdleme20i  31128  cdleme20k  31130  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21a  31136  cdleme21b  31137  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme21f  31143  cdleme21h  31145  cdleme22eALTN  31156  cdleme22f2  31158  cdleme22g  31159  cdleme26e  31170  cdleme26eALTN  31172  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme28a  31181  cdleme28b  31182  cdleme28  31184  cdleme29ex  31185  cdleme29c  31187  cdlemefrs29cpre1  31209  cdlemefr29exN  31213  cdlemefr32sn2aw  31215  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32b  31253  cdleme32d  31255  cdleme32e  31256  cdleme32f  31257  cdleme32le  31258  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme36a  31271  cdleme36m  31272  cdleme37m  31273  cdleme39a  31276  cdleme39n  31277  cdleme40m  31278  cdleme40n  31279  cdleme42e  31290  cdleme42f  31291  cdleme42g  31292  cdleme43bN  31301  cdleme43cN  31302  cdleme43dN  31303  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme17d2  31306  cdleme48b  31314  cdleme4gfv  31318  cdlemeg49le  31322  cdlemeg46c  31324  cdlemeg46fvaw  31327  cdlemeg46nlpq  31328  cdlemeg46frv  31336  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfre  31343  cdleme50trn1  31360  cdleme50trn2a  31361  cdleme50trn2  31362  cdleme  31371  cdlemf  31374  trlord  31380  cdlemg2ce  31403  cdlemg7fvbwN  31418  cdlemg7aN  31436  cdlemg10bALTN  31447  cdlemg10a  31451  cdlemg10  31452  cdlemg12d  31457  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17f  31477  cdlemg17g  31478  cdlemg17h  31479  cdlemg17i  31480  cdlemg17pq  31483  cdlemg17bq  31484  cdlemg17iqN  31485  cdlemg17  31488  cdlemg18d  31492  cdlemg18  31493  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg28a  31504  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg33b0  31512  cdlemg28b  31514  cdlemg28  31515  cdlemg33a  31517  cdlemg33  31522  cdlemg34  31523  cdlemg35  31524  cdlemg36  31525  ltrnco  31530  trlcone  31539  cdlemg44  31544  cdlemg47  31547  cdlemg48  31548  tendococl  31583  tendoplcl  31592  cdlemh1  31626  cdlemi  31631  cdlemj1  31632  cdlemj2  31633  tendocan  31635  cdlemk6  31648  cdlemki  31652  cdlemksat  31657  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkoatnle  31662  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk17  31669  cdlemk1u  31670  cdlemk5u  31672  cdlemk6u  31673  cdlemkuat  31677  cdlemk18  31679  cdlemk19  31680  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk21-2N  31702  cdlemk20-2N  31703  cdlemk22  31704  cdlemk23-3  31713  cdlemk25-3  31715  cdlemk26b-3  31716  cdlemk27-3  31718  cdlemk28-3  31719  cdlemk33N  31720  cdlemk37  31725  cdlemky  31737  cdlemk11ta  31740  cdlemkid3N  31744  cdlemk11tc  31756  cdlemk11t  31757  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk55b  31771  cdlemkyyN  31773  cdlemk55u1  31776  cdlemk55u  31777  cdlemk39u1  31778  cdlemk39u  31779  cdlemk56  31782  cdleml3N  31789  cdleml4N  31790  cdlemm10N  31930  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord10  32035  dihord11c  32036  dihord2pre  32037  dihord4  32070  dihord5apre  32074  dihmeetlem1N  32102  dihglbcpreN  32112  dihjatc1  32123  dihjatc3  32125  dihmeetlem13N  32131  dihmeetlem20N  32138  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmap14lem11  32693  hdmap14lem12  32694
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator