MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp12 Structured version   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  13035  coprimeprodsq  13175  pythagtriplem4  13185  pythagtriplem13  13193  pythagtriplem14  13194  pythagtriplem16  13196  pythagtrip  13200  pceu  13212  mremre  13821  lsmpropd  15301  cmpsublem  17454  isfil2  17880  cxple2a  20582  isosctr  20657  bayesth  24689  brbtwn2  25836  colinearalg  25841  ax5seg  25869  axcontlem4  25898  ofscom  25933  btwndiff  25953  ifscgr  25970  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem12  26024  seglecgr12im  26036  seglecgr12  26037  ivthALT  26329  mzpsubst  26796  monotuz  26995  congmul  27023  congsub  27026  bnj1204  29318  bnj1279  29324  islshpcv  29788  lkrshp  29840  lshpsmreu  29844  lshpkrlem5  29849  cvrval3  30147  4noncolr3  30187  4noncolr2  30188  4noncolr1  30189  athgt  30190  3dimlem2  30193  3dimlem3a  30194  3dimlem4a  30197  3dimlem4  30198  3dimlem4OLDN  30199  1cvratex  30207  hlatexch4  30215  ps-2b  30216  3atlem4  30220  llnnleat  30247  2atm  30261  ps-2c  30262  llnmlplnN  30273  lplnnlelln  30277  2atmat  30295  lvoli2  30315  lvolnlelln  30318  4atlem3b  30332  4atlem10  30340  4atlem11a  30341  4atlem11b  30342  4atlem12a  30344  lplncvrlvol2  30349  2lplnja  30353  dalemswapyz  30390  lneq2at  30512  2lnat  30518  cdlema1N  30525  cdlemb  30528  paddasslem15  30568  pmodlem1  30580  llnmod2i2  30597  llnexchb2lem  30602  dalawlem1  30605  dalawlem3  30607  dalawlem4  30608  dalawlem6  30610  dalawlem7  30611  dalawlem9  30613  dalawlem10  30614  dalawlem11  30615  dalawlem12  30616  dalawlem13  30617  dalawlem15  30619  osumcllem5N  30694  osumcllem6N  30695  osumcllem7N  30696  osumcllem9N  30698  osumcllem10N  30699  osumcllem11N  30700  pl42lem1N  30713  lhpmcvr5N  30761  lhp2atne  30768  lhp2at0ne  30770  4atexlempw  30783  4atexlemex6  30808  4atexlem7  30809  ldilco  30850  ltrneq  30883  trlval2  30897  trlnidat  30907  cdlemd7  30938  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  cdleme20k  31053  cdleme20l1  31054  cdleme20l2  31055  cdleme20l  31056  cdleme20m  31057  cdleme21a  31059  cdleme21b  31060  cdleme21ct  31063  cdleme21d  31064  cdleme21e  31065  cdleme21f  31066  cdleme21h  31068  cdleme21i  31069  cdleme22eALTN  31079  cdleme22f2  31081  cdleme22g  31082  cdleme24  31086  cdleme25a  31087  cdleme25c  31089  cdleme25dN  31090  cdleme26e  31093  cdleme26ee  31094  cdleme26eALTN  31095  cdleme27N  31103  cdleme28a  31104  cdleme28b  31105  cdleme28  31107  cdlemefr32sn2aw  31138  cdlemefs32sn1aw  31148  cdleme43fsv1snlem  31154  cdleme41sn3a  31167  cdleme32c  31177  cdleme32e  31179  cdleme32le  31181  cdleme35a  31182  cdleme35b  31184  cdleme35c  31185  cdleme35e  31187  cdleme35f  31188  cdleme36a  31194  cdleme36m  31195  cdleme39a  31199  cdleme40m  31201  cdleme40n  31202  cdleme43bN  31224  cdleme43dN  31226  cdleme46f2g2  31227  cdleme46f2g1  31228  cdleme17d2  31229  cdleme4gfv  31241  cdlemeg49le  31245  cdlemeg46c  31247  cdlemeg46fvaw  31250  cdlemeg46nlpq  31251  cdlemeg46gfre  31266  cdleme50trn2  31285  cdleme  31294  cdlemg2idN  31330  cdlemg7fvbwN  31341  cdlemg10bALTN  31370  cdlemg10a  31374  cdlemg12d  31380  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg13  31386  cdlemg17b  31396  cdlemg17dN  31397  cdlemg17dALTN  31398  cdlemg17e  31399  cdlemg17f  31400  cdlemg17i  31403  cdlemg17pq  31406  cdlemg17bq  31407  cdlemg17iqN  31408  cdlemg18d  31415  cdlemg18  31416  cdlemg19a  31417  cdlemg19  31418  cdlemg21  31420  cdlemg27a  31426  cdlemg28a  31427  cdlemg31b0N  31428  cdlemg27b  31430  cdlemg31c  31433  cdlemg33b0  31435  cdlemg33c0  31436  cdlemg28  31438  cdlemg33a  31440  cdlemg33  31445  cdlemg36  31448  ltrnco  31453  cdlemg44  31467  cdlemg47  31470  tendococl  31506  tendoplcl  31515  cdlemh1  31549  cdlemh2  31550  cdlemh  31551  cdlemi  31554  tendocan  31558  cdlemk5  31570  cdlemk6  31571  cdlemk7  31582  cdlemk11  31583  cdlemk12  31584  cdlemkole  31587  cdlemk14  31588  cdlemk15  31589  cdlemk16a  31590  cdlemk16  31591  cdlemk18  31602  cdlemk19  31603  cdlemk7u  31604  cdlemk11u  31605  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  cdlemk27-3  31641  cdlemk33N  31643  cdlemk11ta  31663  cdlemkid3N  31667  cdlemk11tc  31679  cdlemk11t  31680  cdlemk45  31681  cdlemk46  31682  cdlemk47  31683  cdlemk48  31684  cdlemk49  31685  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  cdlemk53a  31689  cdlemk55b  31694  cdlemkyyN  31696  cdlemk55u1  31699  cdlemk39u1  31701  cdlemk56  31705  cdlemm10N  31853  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord10  31958  dihord4  31993  dihord5apre  31997  dihglblem2N  32029  dihjatc1  32046  dihjatc2N  32047  dihjatc3  32048  dihmeetlem15N  32056  dihmeetlem20N  32061  mapdpglem24  32439  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