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

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

Proof of Theorem simp13
StepHypRef Expression
1 simp3 959 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl13  1034  simpr13  1043  simp113  1088  simp213  1097  simp313  1106  funtpg  5442  omeu  6765  ackbij1lem16  8049  dvdsgcd  12971  coprimeprodsq  13111  pythagtriplem4  13121  pythagtriplem13  13129  pythagtriplem14  13130  pythagtriplem16  13132  pythagtrip  13136  lsmpropd  15237  isfil2  17810  filuni  17839  ufprim  17863  cxple2a  20458  isosctr  20533  measres  24371  bayesth  24477  brbtwn2  25559  colinearalg  25564  ax5seg  25592  axcontlem4  25621  ofscom  25656  btwndiff  25676  ifscgr  25693  brofs2  25726  brifs2  25727  fscgr  25729  btwnconn1lem1  25736  btwnconn1lem2  25737  btwnconn1lem3  25738  btwnconn1lem4  25739  btwnconn1lem12  25747  seglecgr12im  25759  seglecgr12  25760  ivthALT  26030  mzpsubst  26497  congmul  26724  congsub  26727  islshpcv  29169  eqlkr  29215  lshpsmreu  29225  lshpkrlem5  29230  atlrelat1  29437  cvlcvr1  29455  cvlcvrp  29456  cvlatcvr1  29457  cvlatcvr2  29458  4noncolr3  29568  4noncolr2  29569  4noncolr1  29570  athgt  29571  3dimlem2  29574  3dimlem3a  29575  3dimlem4a  29578  3dimlem4  29579  3dimlem4OLDN  29580  3dim1  29582  3dim2  29583  hlatexch4  29596  ps-2b  29597  3atlem6  29603  llnnleat  29628  2atm  29642  ps-2c  29643  llnmlplnN  29654  2atmat  29676  2llnjN  29682  lvoli2  29696  4atlem3b  29713  4atlem10  29721  4atlem11a  29722  4atlem11b  29723  4atlem12a  29725  4atlem12b  29726  dalemswapyz  29771  lneq2at  29893  2lnat  29899  cdlema1N  29906  cdlemb  29909  pmodlem1  29961  llnmod2i2  29978  dalawlem1  29986  dalawlem3  29988  dalawlem4  29989  dalawlem6  29991  dalawlem9  29994  dalawlem10  29995  dalawlem11  29996  dalawlem12  29997  dalawlem13  29998  dalawlem15  30000  dalaw  30001  pclfinN  30015  osumcllem5N  30075  osumcllem6N  30076  osumcllem7N  30077  osumcllem9N  30079  osumcllem11N  30081  pl42lem1N  30094  lhp2at0  30147  lhp2atne  30149  lhp2at0ne  30151  4atexlem7  30190  ldilco  30231  ltrneq  30264  cdlemd2  30314  cdleme0ex2N  30339  cdleme7aa  30357  cdleme7c  30360  cdleme7d  30361  cdleme7ga  30363  cdleme11c  30376  cdleme11l  30384  cdleme11  30385  cdleme14  30388  cdleme15a  30389  cdleme15c  30391  cdleme16b  30394  cdleme16c  30395  cdleme16d  30396  cdleme16e  30397  cdleme16f  30398  cdleme0nex  30405  cdleme19b  30419  cdleme19d  30421  cdleme19e  30422  cdleme20f  30429  cdleme20k  30434  cdleme20l1  30435  cdleme20l2  30436  cdleme20l  30437  cdleme20m  30438  cdleme21a  30440  cdleme21b  30441  cdleme21c  30442  cdleme21ct  30444  cdleme21d  30445  cdleme21e  30446  cdleme21f  30447  cdleme21i  30450  cdleme22cN  30457  cdleme22eALTN  30460  cdleme25a  30468  cdleme25c  30470  cdleme25dN  30471  cdleme26e  30474  cdleme26ee  30475  cdleme26eALTN  30476  cdleme26f2ALTN  30479  cdleme26f2  30480  cdleme28a  30485  cdleme28b  30486  cdleme28  30488  cdlemefr32sn2aw  30519  cdlemefs32sn1aw  30529  cdleme43fsv1snlem  30535  cdleme41sn3a  30548  cdleme32c  30558  cdleme32e  30560  cdleme32le  30562  cdleme35a  30563  cdleme35b  30565  cdleme35d  30567  cdleme36a  30575  cdleme36m  30576  cdleme39a  30580  cdleme40m  30582  cdleme40n  30583  cdleme43bN  30605  cdleme43dN  30607  cdleme46f2g2  30608  cdleme46f2g1  30609  cdleme4gfv  30622  cdlemeg49le  30626  cdlemeg46c  30628  cdlemeg46fvaw  30631  cdlemeg46nlpq  30632  cdlemeg46gfre  30647  cdleme50trn2  30666  cdlemg2ce  30707  cdlemg2idN  30711  cdlemg7fvbwN  30722  cdlemg10bALTN  30751  cdlemg10a  30755  cdlemg12d  30761  cdlemg12g  30764  cdlemg12  30765  cdlemg13a  30766  cdlemg13  30767  cdlemg17b  30777  cdlemg17dN  30778  cdlemg17dALTN  30779  cdlemg17e  30780  cdlemg17pq  30787  cdlemg17bq  30788  cdlemg18d  30796  cdlemg19a  30798  cdlemg19  30799  cdlemg21  30801  cdlemg27a  30807  cdlemg31b0N  30809  cdlemg27b  30811  cdlemg31c  30814  cdlemg33b0  30816  cdlemg33c0  30817  cdlemg28b  30818  cdlemg33a  30821  cdlemg33  30826  ltrnco  30834  cdlemg44  30848  cdlemg47  30851  tendococl  30887  tendoplcl  30896  cdlemh1  30930  cdlemh2  30931  cdlemh  30932  cdlemi  30935  cdlemk5  30951  cdlemk6  30952  cdlemksel  30960  cdlemksv2  30962  cdlemk7  30963  cdlemk11  30964  cdlemk12  30965  cdlemkole  30968  cdlemk14  30969  cdlemk15  30970  cdlemk16a  30971  cdlemk16  30972  cdlemk1u  30974  cdlemk5u  30976  cdlemk6u  30977  cdlemkuel  30980  cdlemkuv2  30982  cdlemk18  30983  cdlemk19  30984  cdlemk7u  30985  cdlemk11u  30986  cdlemk12u  30987  cdlemk21N  30988  cdlemk20  30989  cdlemkoatnle-2N  30990  cdlemk13-2N  30991  cdlemkole-2N  30992  cdlemk14-2N  30993  cdlemk15-2N  30994  cdlemk16-2N  30995  cdlemk17-2N  30996  cdlemk18-2N  31001  cdlemk19-2N  31002  cdlemk7u-2N  31003  cdlemk11u-2N  31004  cdlemk12u-2N  31005  cdlemk21-2N  31006  cdlemk20-2N  31007  cdlemkuel-3  31013  cdlemkuv2-3N  31014  cdlemk22-3  31016  cdlemk33N  31024  cdlemk47  31064  cdlemk48  31065  cdlemk49  31066  cdlemk50  31067  cdlemk51  31068  cdlemk52  31069  cdlemk53a  31070  cdlemk55b  31075  cdlemkyyN  31077  cdlemk55u1  31080  cdlemk39u1  31082  cdlemk56  31086  dihord1  31334  dihord2a  31335  dihord10  31339  dihord11c  31340  dihord4  31374  dihord5apre  31378  dihglblem2N  31410  dihglbcpreN  31416  dihmeetlem3N  31421  dihjatc1  31427  dihjatc2N  31428  dihjatc3  31429  mapdpglem24  31820  baerlem3lem2  31826  baerlem5alem2  31827  baerlem5blem2  31828  hdmap14lem11  31997  hdmap14lem12  31998  hdmapglem7  32048
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