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

Theorem simp12 986
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp12  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )

Proof of Theorem simp12
StepHypRef Expression
1 simp2 956 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl12  1031  simpr12  1040  simp112  1085  simp212  1094  simp312  1103  dvdsgcd  12738  coprimeprodsq  12878  pythagtriplem4  12888  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  pythagtrip  12903  pceu  12915  mremre  13522  lsmpropd  15002  cmpsublem  17142  isfil2  17567  cxple2a  20062  isosctr  20137  bayesth  23657  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axcontlem4  24667  ofscom  24702  btwndiff  24722  ifscgr  24739  brofs2  24772  brifs2  24773  fscgr  24775  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem12  24793  seglecgr12im  24805  seglecgr12  24806  prdnei  25676  limptlimpr2lem1  25677  islimrs3  25684  islimrs4  25685  isibg1a6  26228  ivthALT  26361  mzpsubst  26929  monotuz  27129  congmul  27157  congsub  27160  bnj1204  29358  bnj1279  29364  islshpcv  29865  lkrshp  29917  lshpsmreu  29921  lshpkrlem5  29926  cvrval3  30224  4noncolr3  30264  4noncolr2  30265  4noncolr1  30266  athgt  30267  3dimlem2  30270  3dimlem3a  30271  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  1cvratex  30284  hlatexch4  30292  ps-2b  30293  3atlem4  30297  llnnleat  30324  2atm  30338  ps-2c  30339  llnmlplnN  30350  lplnnlelln  30354  2atmat  30372  lvoli2  30392  lvolnlelln  30395  4atlem3b  30409  4atlem10  30417  4atlem11a  30418  4atlem11b  30419  4atlem12a  30421  lplncvrlvol2  30426  2lplnja  30430  dalemswapyz  30467  lneq2at  30589  2lnat  30595  cdlema1N  30602  cdlemb  30605  paddasslem15  30645  pmodlem1  30657  llnmod2i2  30674  llnexchb2lem  30679  dalawlem1  30682  dalawlem3  30684  dalawlem4  30685  dalawlem6  30687  dalawlem7  30688  dalawlem9  30690  dalawlem10  30691  dalawlem11  30692  dalawlem12  30693  dalawlem13  30694  dalawlem15  30696  osumcllem5N  30771  osumcllem6N  30772  osumcllem7N  30773  osumcllem9N  30775  osumcllem10N  30776  osumcllem11N  30777  pl42lem1N  30790  lhpmcvr5N  30838  lhp2atne  30845  lhp2at0ne  30847  4atexlempw  30860  4atexlemex6  30885  4atexlem7  30886  ldilco  30927  ltrneq  30960  trlval2  30974  trlnidat  30984  cdlemd7  31015  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  cdleme20k  31130  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21a  31136  cdleme21b  31137  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme21f  31143  cdleme21h  31145  cdleme21i  31146  cdleme22eALTN  31156  cdleme22f2  31158  cdleme22g  31159  cdleme24  31163  cdleme25a  31164  cdleme25c  31166  cdleme25dN  31167  cdleme26e  31170  cdleme26ee  31171  cdleme26eALTN  31172  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme28  31184  cdlemefr32sn2aw  31215  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32c  31254  cdleme32e  31256  cdleme32le  31258  cdleme35a  31259  cdleme35b  31261  cdleme35c  31262  cdleme35e  31264  cdleme35f  31265  cdleme36a  31271  cdleme36m  31272  cdleme39a  31276  cdleme40m  31278  cdleme40n  31279  cdleme43bN  31301  cdleme43dN  31303  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme17d2  31306  cdleme4gfv  31318  cdlemeg49le  31322  cdlemeg46c  31324  cdlemeg46fvaw  31327  cdlemeg46nlpq  31328  cdlemeg46gfre  31343  cdleme50trn2  31362  cdleme  31371  cdlemg2idN  31407  cdlemg7fvbwN  31418  cdlemg10bALTN  31447  cdlemg10a  31451  cdlemg12d  31457  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17f  31477  cdlemg17i  31480  cdlemg17pq  31483  cdlemg17bq  31484  cdlemg17iqN  31485  cdlemg18d  31492  cdlemg18  31493  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg28a  31504  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33c0  31513  cdlemg28  31515  cdlemg33a  31517  cdlemg33  31522  cdlemg36  31525  ltrnco  31530  cdlemg44  31544  cdlemg47  31547  tendococl  31583  tendoplcl  31592  cdlemh1  31626  cdlemh2  31627  cdlemh  31628  cdlemi  31631  tendocan  31635  cdlemk5  31647  cdlemk6  31648  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  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  cdlemk27-3  31718  cdlemk33N  31720  cdlemk11ta  31740  cdlemkid3N  31744  cdlemk11tc  31756  cdlemk11t  31757  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk55b  31771  cdlemkyyN  31773  cdlemk55u1  31776  cdlemk39u1  31778  cdlemk56  31782  cdlemm10N  31930  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord10  32035  dihord4  32070  dihord5apre  32074  dihglblem2N  32106  dihjatc1  32123  dihjatc2N  32124  dihjatc3  32125  dihmeetlem15N  32133  dihmeetlem20N  32138  mapdpglem24  32516  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