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  5460  omeu  6787  ackbij1lem16  8071  dvdsgcd  12998  coprimeprodsq  13138  pythagtriplem4  13148  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pythagtrip  13163  lsmpropd  15264  isfil2  17841  filuni  17870  ufprim  17894  cxple2a  20543  isosctr  20618  measres  24529  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  congmul  26922  congsub  26925  islshpcv  29536  eqlkr  29582  lshpsmreu  29592  lshpkrlem5  29597  atlrelat1  29804  cvlcvr1  29822  cvlcvrp  29823  cvlatcvr1  29824  cvlatcvr2  29825  4noncolr3  29935  4noncolr2  29936  4noncolr1  29937  athgt  29938  3dimlem2  29941  3dimlem3a  29942  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  3dim1  29949  3dim2  29950  hlatexch4  29963  ps-2b  29964  3atlem6  29970  llnnleat  29995  2atm  30009  ps-2c  30010  llnmlplnN  30021  2atmat  30043  2llnjN  30049  lvoli2  30063  4atlem3b  30080  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem12a  30092  4atlem12b  30093  dalemswapyz  30138  lneq2at  30260  2lnat  30266  cdlema1N  30273  cdlemb  30276  pmodlem1  30328  llnmod2i2  30345  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem6  30358  dalawlem9  30361  dalawlem10  30362  dalawlem11  30363  dalawlem12  30364  dalawlem13  30365  dalawlem15  30367  dalaw  30368  pclfinN  30382  osumcllem5N  30442  osumcllem6N  30443  osumcllem7N  30444  osumcllem9N  30446  osumcllem11N  30448  pl42lem1N  30461  lhp2at0  30514  lhp2atne  30516  lhp2at0ne  30518  4atexlem7  30557  ldilco  30598  ltrneq  30631  cdlemd2  30681  cdleme0ex2N  30706  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7ga  30730  cdleme11c  30743  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme0nex  30772  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20f  30796  cdleme20k  30801  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21a  30807  cdleme21b  30808  cdleme21c  30809  cdleme21ct  30811  cdleme21d  30812  cdleme21e  30813  cdleme21f  30814  cdleme21i  30817  cdleme22cN  30824  cdleme22eALTN  30827  cdleme25a  30835  cdleme25c  30837  cdleme25dN  30838  cdleme26e  30841  cdleme26ee  30842  cdleme26eALTN  30843  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme28a  30852  cdleme28b  30853  cdleme28  30855  cdlemefr32sn2aw  30886  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32c  30925  cdleme32e  30927  cdleme32le  30929  cdleme35a  30930  cdleme35b  30932  cdleme35d  30934  cdleme36a  30942  cdleme36m  30943  cdleme39a  30947  cdleme40m  30949  cdleme40n  30950  cdleme43bN  30972  cdleme43dN  30974  cdleme46f2g2  30975  cdleme46f2g1  30976  cdleme4gfv  30989  cdlemeg49le  30993  cdlemeg46c  30995  cdlemeg46fvaw  30998  cdlemeg46nlpq  30999  cdlemeg46gfre  31014  cdleme50trn2  31033  cdlemg2ce  31074  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  cdlemg17pq  31154  cdlemg17bq  31155  cdlemg18d  31163  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33c0  31184  cdlemg28b  31185  cdlemg33a  31188  cdlemg33  31193  ltrnco  31201  cdlemg44  31215  cdlemg47  31218  tendococl  31254  tendoplcl  31263  cdlemh1  31297  cdlemh2  31298  cdlemh  31299  cdlemi  31302  cdlemk5  31318  cdlemk6  31319  cdlemksel  31327  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk16a  31338  cdlemk16  31339  cdlemk1u  31341  cdlemk5u  31343  cdlemk6u  31344  cdlemkuel  31347  cdlemkuv2  31349  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  cdlemkuel-3  31380  cdlemkuv2-3N  31381  cdlemk22-3  31383  cdlemk33N  31391  cdlemk47  31431  cdlemk48  31432  cdlemk49  31433  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdlemk55b  31442  cdlemkyyN  31444  cdlemk55u1  31447  cdlemk39u1  31449  cdlemk56  31453  dihord1  31701  dihord2a  31702  dihord10  31706  dihord11c  31707  dihord4  31741  dihord5apre  31745  dihglblem2N  31777  dihglbcpreN  31783  dihmeetlem3N  31788  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  mapdpglem24  32187  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmap14lem11  32364  hdmap14lem12  32365  hdmapglem7  32415
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