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  12998  coprimeprodsq  13138  pythagtriplem4  13148  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pythagtrip  13163  pceu  13175  mremre  13784  lsmpropd  15264  cmpsublem  17416  isfil2  17841  cxple2a  20543  isosctr  20618  bayesth  24650  brbtwn2  25748  colinearalg  25753  ax5seg  25781  axcontlem4  25810  ofscom  25845  btwndiff  25865  ifscgr  25882  brofs2  25915  brifs2  25916  fscgr  25918  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem12  25936  seglecgr12im  25948  seglecgr12  25949  ivthALT  26228  mzpsubst  26695  monotuz  26894  congmul  26922  congsub  26925  bnj1204  29087  bnj1279  29093  islshpcv  29536  lkrshp  29588  lshpsmreu  29592  lshpkrlem5  29597  cvrval3  29895  4noncolr3  29935  4noncolr2  29936  4noncolr1  29937  athgt  29938  3dimlem2  29941  3dimlem3a  29942  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  1cvratex  29955  hlatexch4  29963  ps-2b  29964  3atlem4  29968  llnnleat  29995  2atm  30009  ps-2c  30010  llnmlplnN  30021  lplnnlelln  30025  2atmat  30043  lvoli2  30063  lvolnlelln  30066  4atlem3b  30080  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem12a  30092  lplncvrlvol2  30097  2lplnja  30101  dalemswapyz  30138  lneq2at  30260  2lnat  30266  cdlema1N  30273  cdlemb  30276  paddasslem15  30316  pmodlem1  30328  llnmod2i2  30345  llnexchb2lem  30350  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem6  30358  dalawlem7  30359  dalawlem9  30361  dalawlem10  30362  dalawlem11  30363  dalawlem12  30364  dalawlem13  30365  dalawlem15  30367  osumcllem5N  30442  osumcllem6N  30443  osumcllem7N  30444  osumcllem9N  30446  osumcllem10N  30447  osumcllem11N  30448  pl42lem1N  30461  lhpmcvr5N  30509  lhp2atne  30516  lhp2at0ne  30518  4atexlempw  30531  4atexlemex6  30556  4atexlem7  30557  ldilco  30598  ltrneq  30631  trlval2  30645  trlnidat  30655  cdlemd7  30686  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11c  30743  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme0nex  30772  cdleme18d  30777  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20f  30796  cdleme20k  30801  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21a  30807  cdleme21b  30808  cdleme21ct  30811  cdleme21d  30812  cdleme21e  30813  cdleme21f  30814  cdleme21h  30816  cdleme21i  30817  cdleme22eALTN  30827  cdleme22f2  30829  cdleme22g  30830  cdleme24  30834  cdleme25a  30835  cdleme25c  30837  cdleme25dN  30838  cdleme26e  30841  cdleme26ee  30842  cdleme26eALTN  30843  cdleme27N  30851  cdleme28a  30852  cdleme28b  30853  cdleme28  30855  cdlemefr32sn2aw  30886  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32c  30925  cdleme32e  30927  cdleme32le  30929  cdleme35a  30930  cdleme35b  30932  cdleme35c  30933  cdleme35e  30935  cdleme35f  30936  cdleme36a  30942  cdleme36m  30943  cdleme39a  30947  cdleme40m  30949  cdleme40n  30950  cdleme43bN  30972  cdleme43dN  30974  cdleme46f2g2  30975  cdleme46f2g1  30976  cdleme17d2  30977  cdleme4gfv  30989  cdlemeg49le  30993  cdlemeg46c  30995  cdlemeg46fvaw  30998  cdlemeg46nlpq  30999  cdlemeg46gfre  31014  cdleme50trn2  31033  cdleme  31042  cdlemg2idN  31078  cdlemg7fvbwN  31089  cdlemg10bALTN  31118  cdlemg10a  31122  cdlemg12d  31128  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg17b  31144  cdlemg17dN  31145  cdlemg17dALTN  31146  cdlemg17e  31147  cdlemg17f  31148  cdlemg17i  31151  cdlemg17pq  31154  cdlemg17bq  31155  cdlemg17iqN  31156  cdlemg18d  31163  cdlemg18  31164  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg28a  31175  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33c0  31184  cdlemg28  31186  cdlemg33a  31188  cdlemg33  31193  cdlemg36  31196  ltrnco  31201  cdlemg44  31215  cdlemg47  31218  tendococl  31254  tendoplcl  31263  cdlemh1  31297  cdlemh2  31298  cdlemh  31299  cdlemi  31302  tendocan  31306  cdlemk5  31318  cdlemk6  31319  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk16a  31338  cdlemk16  31339  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk21N  31355  cdlemk20  31356  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk21-2N  31373  cdlemk20-2N  31374  cdlemk22  31375  cdlemk27-3  31389  cdlemk33N  31391  cdlemk11ta  31411  cdlemkid3N  31415  cdlemk11tc  31427  cdlemk11t  31428  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk48  31432  cdlemk49  31433  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdlemk55b  31442  cdlemkyyN  31444  cdlemk55u1  31447  cdlemk39u1  31449  cdlemk56  31453  cdlemm10N  31601  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord10  31706  dihord4  31741  dihord5apre  31745  dihglblem2N  31777  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  dihmeetlem15N  31804  dihmeetlem20N  31809  mapdpglem24  32187  hdmap14lem11  32364  hdmap14lem12  32365
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