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

Theorem simp12 988
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl12  1033  simpr12  1042  simp112  1087  simp212  1096  simp312  1105  dvdsgcd  12970  coprimeprodsq  13110  pythagtriplem4  13120  pythagtriplem13  13128  pythagtriplem14  13129  pythagtriplem16  13131  pythagtrip  13135  pceu  13147  mremre  13756  lsmpropd  15236  cmpsublem  17384  isfil2  17809  cxple2a  20457  isosctr  20532  bayesth  24476  brbtwn2  25558  colinearalg  25563  ax5seg  25591  axcontlem4  25620  ofscom  25655  btwndiff  25675  ifscgr  25692  brofs2  25725  brifs2  25726  fscgr  25728  btwnconn1lem1  25735  btwnconn1lem2  25736  btwnconn1lem3  25737  btwnconn1lem4  25738  btwnconn1lem12  25746  seglecgr12im  25758  seglecgr12  25759  ivthALT  26029  mzpsubst  26496  monotuz  26695  congmul  26723  congsub  26726  bnj1204  28719  bnj1279  28725  islshpcv  29168  lkrshp  29220  lshpsmreu  29224  lshpkrlem5  29229  cvrval3  29527  4noncolr3  29567  4noncolr2  29568  4noncolr1  29569  athgt  29570  3dimlem2  29573  3dimlem3a  29574  3dimlem4a  29577  3dimlem4  29578  3dimlem4OLDN  29579  1cvratex  29587  hlatexch4  29595  ps-2b  29596  3atlem4  29600  llnnleat  29627  2atm  29641  ps-2c  29642  llnmlplnN  29653  lplnnlelln  29657  2atmat  29675  lvoli2  29695  lvolnlelln  29698  4atlem3b  29712  4atlem10  29720  4atlem11a  29721  4atlem11b  29722  4atlem12a  29724  lplncvrlvol2  29729  2lplnja  29733  dalemswapyz  29770  lneq2at  29892  2lnat  29898  cdlema1N  29905  cdlemb  29908  paddasslem15  29948  pmodlem1  29960  llnmod2i2  29977  llnexchb2lem  29982  dalawlem1  29985  dalawlem3  29987  dalawlem4  29988  dalawlem6  29990  dalawlem7  29991  dalawlem9  29993  dalawlem10  29994  dalawlem11  29995  dalawlem12  29996  dalawlem13  29997  dalawlem15  29999  osumcllem5N  30074  osumcllem6N  30075  osumcllem7N  30076  osumcllem9N  30078  osumcllem10N  30079  osumcllem11N  30080  pl42lem1N  30093  lhpmcvr5N  30141  lhp2atne  30148  lhp2at0ne  30150  4atexlempw  30163  4atexlemex6  30188  4atexlem7  30189  ldilco  30230  ltrneq  30263  trlval2  30277  trlnidat  30287  cdlemd7  30318  cdleme7aa  30356  cdleme7c  30359  cdleme7d  30360  cdleme7e  30361  cdleme7ga  30362  cdleme7  30363  cdleme11c  30375  cdleme11e  30377  cdleme11l  30383  cdleme11  30384  cdleme14  30387  cdleme15a  30388  cdleme15c  30390  cdleme16b  30393  cdleme16c  30394  cdleme16d  30395  cdleme16e  30396  cdleme16f  30397  cdleme0nex  30404  cdleme18d  30409  cdleme19b  30418  cdleme19d  30420  cdleme19e  30421  cdleme20f  30428  cdleme20k  30433  cdleme20l1  30434  cdleme20l2  30435  cdleme20l  30436  cdleme20m  30437  cdleme21a  30439  cdleme21b  30440  cdleme21ct  30443  cdleme21d  30444  cdleme21e  30445  cdleme21f  30446  cdleme21h  30448  cdleme21i  30449  cdleme22eALTN  30459  cdleme22f2  30461  cdleme22g  30462  cdleme24  30466  cdleme25a  30467  cdleme25c  30469  cdleme25dN  30470  cdleme26e  30473  cdleme26ee  30474  cdleme26eALTN  30475  cdleme27N  30483  cdleme28a  30484  cdleme28b  30485  cdleme28  30487  cdlemefr32sn2aw  30518  cdlemefs32sn1aw  30528  cdleme43fsv1snlem  30534  cdleme41sn3a  30547  cdleme32c  30557  cdleme32e  30559  cdleme32le  30561  cdleme35a  30562  cdleme35b  30564  cdleme35c  30565  cdleme35e  30567  cdleme35f  30568  cdleme36a  30574  cdleme36m  30575  cdleme39a  30579  cdleme40m  30581  cdleme40n  30582  cdleme43bN  30604  cdleme43dN  30606  cdleme46f2g2  30607  cdleme46f2g1  30608  cdleme17d2  30609  cdleme4gfv  30621  cdlemeg49le  30625  cdlemeg46c  30627  cdlemeg46fvaw  30630  cdlemeg46nlpq  30631  cdlemeg46gfre  30646  cdleme50trn2  30665  cdleme  30674  cdlemg2idN  30710  cdlemg7fvbwN  30721  cdlemg10bALTN  30750  cdlemg10a  30754  cdlemg12d  30760  cdlemg12g  30763  cdlemg12  30764  cdlemg13a  30765  cdlemg13  30766  cdlemg17b  30776  cdlemg17dN  30777  cdlemg17dALTN  30778  cdlemg17e  30779  cdlemg17f  30780  cdlemg17i  30783  cdlemg17pq  30786  cdlemg17bq  30787  cdlemg17iqN  30788  cdlemg18d  30795  cdlemg18  30796  cdlemg19a  30797  cdlemg19  30798  cdlemg21  30800  cdlemg27a  30806  cdlemg28a  30807  cdlemg31b0N  30808  cdlemg27b  30810  cdlemg31c  30813  cdlemg33b0  30815  cdlemg33c0  30816  cdlemg28  30818  cdlemg33a  30820  cdlemg33  30825  cdlemg36  30828  ltrnco  30833  cdlemg44  30847  cdlemg47  30850  tendococl  30886  tendoplcl  30895  cdlemh1  30929  cdlemh2  30930  cdlemh  30931  cdlemi  30934  tendocan  30938  cdlemk5  30950  cdlemk6  30951  cdlemk7  30962  cdlemk11  30963  cdlemk12  30964  cdlemkole  30967  cdlemk14  30968  cdlemk15  30969  cdlemk16a  30970  cdlemk16  30971  cdlemk18  30982  cdlemk19  30983  cdlemk7u  30984  cdlemk11u  30985  cdlemk12u  30986  cdlemk21N  30987  cdlemk20  30988  cdlemkoatnle-2N  30989  cdlemk13-2N  30990  cdlemkole-2N  30991  cdlemk14-2N  30992  cdlemk15-2N  30993  cdlemk16-2N  30994  cdlemk17-2N  30995  cdlemk18-2N  31000  cdlemk19-2N  31001  cdlemk7u-2N  31002  cdlemk11u-2N  31003  cdlemk12u-2N  31004  cdlemk21-2N  31005  cdlemk20-2N  31006  cdlemk22  31007  cdlemk27-3  31021  cdlemk33N  31023  cdlemk11ta  31043  cdlemkid3N  31047  cdlemk11tc  31059  cdlemk11t  31060  cdlemk45  31061  cdlemk46  31062  cdlemk47  31063  cdlemk48  31064  cdlemk49  31065  cdlemk50  31066  cdlemk51  31067  cdlemk52  31068  cdlemk53a  31069  cdlemk55b  31074  cdlemkyyN  31076  cdlemk55u1  31079  cdlemk39u1  31081  cdlemk56  31085  cdlemm10N  31233  dihord1  31333  dihord2a  31334  dihord2b  31335  dihord10  31338  dihord4  31373  dihord5apre  31377  dihglblem2N  31409  dihjatc1  31426  dihjatc2N  31427  dihjatc3  31428  dihmeetlem15N  31436  dihmeetlem20N  31441  mapdpglem24  31819  hdmap14lem11  31996  hdmap14lem12  31997
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