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  5492  omeu  6819  ackbij1lem16  8104  dvdsgcd  13031  coprimeprodsq  13171  pythagtriplem4  13181  pythagtriplem13  13189  pythagtriplem14  13190  pythagtriplem16  13192  pythagtrip  13196  lsmpropd  15297  isfil2  17876  filuni  17905  ufprim  17929  cxple2a  20578  isosctr  20653  measres  24564  bayesth  24685  brbtwn2  25792  colinearalg  25797  ax5seg  25825  axcontlem4  25854  ofscom  25889  btwndiff  25909  ifscgr  25926  brofs2  25959  brifs2  25960  fscgr  25962  btwnconn1lem1  25969  btwnconn1lem2  25970  btwnconn1lem3  25971  btwnconn1lem4  25972  btwnconn1lem12  25980  seglecgr12im  25992  seglecgr12  25993  ivthALT  26275  mzpsubst  26742  congmul  26969  congsub  26972  islshpcv  29690  eqlkr  29736  lshpsmreu  29746  lshpkrlem5  29751  atlrelat1  29958  cvlcvr1  29976  cvlcvrp  29977  cvlatcvr1  29978  cvlatcvr2  29979  4noncolr3  30089  4noncolr2  30090  4noncolr1  30091  athgt  30092  3dimlem2  30095  3dimlem3a  30096  3dimlem4a  30099  3dimlem4  30100  3dimlem4OLDN  30101  3dim1  30103  3dim2  30104  hlatexch4  30117  ps-2b  30118  3atlem6  30124  llnnleat  30149  2atm  30163  ps-2c  30164  llnmlplnN  30175  2atmat  30197  2llnjN  30203  lvoli2  30217  4atlem3b  30234  4atlem10  30242  4atlem11a  30243  4atlem11b  30244  4atlem12a  30246  4atlem12b  30247  dalemswapyz  30292  lneq2at  30414  2lnat  30420  cdlema1N  30427  cdlemb  30430  pmodlem1  30482  llnmod2i2  30499  dalawlem1  30507  dalawlem3  30509  dalawlem4  30510  dalawlem6  30512  dalawlem9  30515  dalawlem10  30516  dalawlem11  30517  dalawlem12  30518  dalawlem13  30519  dalawlem15  30521  dalaw  30522  pclfinN  30536  osumcllem5N  30596  osumcllem6N  30597  osumcllem7N  30598  osumcllem9N  30600  osumcllem11N  30602  pl42lem1N  30615  lhp2at0  30668  lhp2atne  30670  lhp2at0ne  30672  4atexlem7  30711  ldilco  30752  ltrneq  30785  cdlemd2  30835  cdleme0ex2N  30860  cdleme7aa  30878  cdleme7c  30881  cdleme7d  30882  cdleme7ga  30884  cdleme11c  30897  cdleme11l  30905  cdleme11  30906  cdleme14  30909  cdleme15a  30910  cdleme15c  30912  cdleme16b  30915  cdleme16c  30916  cdleme16d  30917  cdleme16e  30918  cdleme16f  30919  cdleme0nex  30926  cdleme19b  30940  cdleme19d  30942  cdleme19e  30943  cdleme20f  30950  cdleme20k  30955  cdleme20l1  30956  cdleme20l2  30957  cdleme20l  30958  cdleme20m  30959  cdleme21a  30961  cdleme21b  30962  cdleme21c  30963  cdleme21ct  30965  cdleme21d  30966  cdleme21e  30967  cdleme21f  30968  cdleme21i  30971  cdleme22cN  30978  cdleme22eALTN  30981  cdleme25a  30989  cdleme25c  30991  cdleme25dN  30992  cdleme26e  30995  cdleme26ee  30996  cdleme26eALTN  30997  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme28a  31006  cdleme28b  31007  cdleme28  31009  cdlemefr32sn2aw  31040  cdlemefs32sn1aw  31050  cdleme43fsv1snlem  31056  cdleme41sn3a  31069  cdleme32c  31079  cdleme32e  31081  cdleme32le  31083  cdleme35a  31084  cdleme35b  31086  cdleme35d  31088  cdleme36a  31096  cdleme36m  31097  cdleme39a  31101  cdleme40m  31103  cdleme40n  31104  cdleme43bN  31126  cdleme43dN  31128  cdleme46f2g2  31129  cdleme46f2g1  31130  cdleme4gfv  31143  cdlemeg49le  31147  cdlemeg46c  31149  cdlemeg46fvaw  31152  cdlemeg46nlpq  31153  cdlemeg46gfre  31168  cdleme50trn2  31187  cdlemg2ce  31228  cdlemg2idN  31232  cdlemg7fvbwN  31243  cdlemg10bALTN  31272  cdlemg10a  31276  cdlemg12d  31282  cdlemg12g  31285  cdlemg12  31286  cdlemg13a  31287  cdlemg13  31288  cdlemg17b  31298  cdlemg17dN  31299  cdlemg17dALTN  31300  cdlemg17e  31301  cdlemg17pq  31308  cdlemg17bq  31309  cdlemg18d  31317  cdlemg19a  31319  cdlemg19  31320  cdlemg21  31322  cdlemg27a  31328  cdlemg31b0N  31330  cdlemg27b  31332  cdlemg31c  31335  cdlemg33b0  31337  cdlemg33c0  31338  cdlemg28b  31339  cdlemg33a  31342  cdlemg33  31347  ltrnco  31355  cdlemg44  31369  cdlemg47  31372  tendococl  31408  tendoplcl  31417  cdlemh1  31451  cdlemh2  31452  cdlemh  31453  cdlemi  31456  cdlemk5  31472  cdlemk6  31473  cdlemksel  31481  cdlemksv2  31483  cdlemk7  31484  cdlemk11  31485  cdlemk12  31486  cdlemkole  31489  cdlemk14  31490  cdlemk15  31491  cdlemk16a  31492  cdlemk16  31493  cdlemk1u  31495  cdlemk5u  31497  cdlemk6u  31498  cdlemkuel  31501  cdlemkuv2  31503  cdlemk18  31504  cdlemk19  31505  cdlemk7u  31506  cdlemk11u  31507  cdlemk12u  31508  cdlemk21N  31509  cdlemk20  31510  cdlemkoatnle-2N  31511  cdlemk13-2N  31512  cdlemkole-2N  31513  cdlemk14-2N  31514  cdlemk15-2N  31515  cdlemk16-2N  31516  cdlemk17-2N  31517  cdlemk18-2N  31522  cdlemk19-2N  31523  cdlemk7u-2N  31524  cdlemk11u-2N  31525  cdlemk12u-2N  31526  cdlemk21-2N  31527  cdlemk20-2N  31528  cdlemkuel-3  31534  cdlemkuv2-3N  31535  cdlemk22-3  31537  cdlemk33N  31545  cdlemk47  31585  cdlemk48  31586  cdlemk49  31587  cdlemk50  31588  cdlemk51  31589  cdlemk52  31590  cdlemk53a  31591  cdlemk55b  31596  cdlemkyyN  31598  cdlemk55u1  31601  cdlemk39u1  31603  cdlemk56  31607  dihord1  31855  dihord2a  31856  dihord10  31860  dihord11c  31861  dihord4  31895  dihord5apre  31899  dihglblem2N  31931  dihglbcpreN  31937  dihmeetlem3N  31942  dihjatc1  31948  dihjatc2N  31949  dihjatc3  31950  mapdpglem24  32341  baerlem3lem2  32347  baerlem5alem2  32348  baerlem5blem2  32349  hdmap14lem11  32518  hdmap14lem12  32519  hdmapglem7  32569
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