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

Theorem simp13 987
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl13  1032  simpr13  1041  simp113  1086  simp213  1095  simp313  1104  omeu  6585  ackbij1lem16  7863  dvdsgcd  12724  coprimeprodsq  12864  pythagtriplem4  12874  pythagtriplem13  12882  pythagtriplem14  12883  pythagtriplem16  12885  pythagtrip  12889  lsmpropd  14988  isfil2  17553  filuni  17582  ufprim  17606  cxple2a  20048  isosctr  20123  measres  23551  bayesth  23644  brbtwn2  24535  colinearalg  24540  ax5seg  24568  axcontlem4  24597  ofscom  24632  btwndiff  24652  ifscgr  24669  brofs2  24702  brifs2  24703  fscgr  24705  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem12  24723  seglecgr12im  24735  seglecgr12  24736  intcont  25554  islimrs3  25592  islimrs4  25593  isibg1a6  26136  ivthALT  26269  mzpsubst  26837  congmul  27065  congsub  27068  islshpcv  29316  eqlkr  29362  lshpsmreu  29372  lshpkrlem5  29377  atlrelat1  29584  cvlcvr1  29602  cvlcvrp  29603  cvlatcvr1  29604  cvlatcvr2  29605  4noncolr3  29715  4noncolr2  29716  4noncolr1  29717  athgt  29718  3dimlem2  29721  3dimlem3a  29722  3dimlem4a  29725  3dimlem4  29726  3dimlem4OLDN  29727  3dim1  29729  3dim2  29730  hlatexch4  29743  ps-2b  29744  3atlem6  29750  llnnleat  29775  2atm  29789  ps-2c  29790  llnmlplnN  29801  2atmat  29823  2llnjN  29829  lvoli2  29843  4atlem3b  29860  4atlem10  29868  4atlem11a  29869  4atlem11b  29870  4atlem12a  29872  4atlem12b  29873  dalemswapyz  29918  lneq2at  30040  2lnat  30046  cdlema1N  30053  cdlemb  30056  pmodlem1  30108  llnmod2i2  30125  dalawlem1  30133  dalawlem3  30135  dalawlem4  30136  dalawlem6  30138  dalawlem9  30141  dalawlem10  30142  dalawlem11  30143  dalawlem12  30144  dalawlem13  30145  dalawlem15  30147  dalaw  30148  pclfinN  30162  osumcllem5N  30222  osumcllem6N  30223  osumcllem7N  30224  osumcllem9N  30226  osumcllem11N  30228  pl42lem1N  30241  lhp2at0  30294  lhp2atne  30296  lhp2at0ne  30298  4atexlem7  30337  ldilco  30378  ltrneq  30411  cdlemd2  30461  cdleme0ex2N  30486  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7ga  30510  cdleme11c  30523  cdleme11l  30531  cdleme11  30532  cdleme14  30535  cdleme15a  30536  cdleme15c  30538  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme0nex  30552  cdleme19b  30566  cdleme19d  30568  cdleme19e  30569  cdleme20f  30576  cdleme20k  30581  cdleme20l1  30582  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21a  30587  cdleme21b  30588  cdleme21c  30589  cdleme21ct  30591  cdleme21d  30592  cdleme21e  30593  cdleme21f  30594  cdleme21i  30597  cdleme22cN  30604  cdleme22eALTN  30607  cdleme25a  30615  cdleme25c  30617  cdleme25dN  30618  cdleme26e  30621  cdleme26ee  30622  cdleme26eALTN  30623  cdleme26f2ALTN  30626  cdleme26f2  30627  cdleme28a  30632  cdleme28b  30633  cdleme28  30635  cdlemefr32sn2aw  30666  cdlemefs32sn1aw  30676  cdleme43fsv1snlem  30682  cdleme41sn3a  30695  cdleme32c  30705  cdleme32e  30707  cdleme32le  30709  cdleme35a  30710  cdleme35b  30712  cdleme35d  30714  cdleme36a  30722  cdleme36m  30723  cdleme39a  30727  cdleme40m  30729  cdleme40n  30730  cdleme43bN  30752  cdleme43dN  30754  cdleme46f2g2  30755  cdleme46f2g1  30756  cdleme4gfv  30769  cdlemeg49le  30773  cdlemeg46c  30775  cdlemeg46fvaw  30778  cdlemeg46nlpq  30779  cdlemeg46gfre  30794  cdleme50trn2  30813  cdlemg2ce  30854  cdlemg2idN  30858  cdlemg7fvbwN  30869  cdlemg10bALTN  30898  cdlemg10a  30902  cdlemg12d  30908  cdlemg12g  30911  cdlemg12  30912  cdlemg13a  30913  cdlemg13  30914  cdlemg17b  30924  cdlemg17dN  30925  cdlemg17dALTN  30926  cdlemg17e  30927  cdlemg17pq  30934  cdlemg17bq  30935  cdlemg18d  30943  cdlemg19a  30945  cdlemg19  30946  cdlemg21  30948  cdlemg27a  30954  cdlemg31b0N  30956  cdlemg27b  30958  cdlemg31c  30961  cdlemg33b0  30963  cdlemg33c0  30964  cdlemg28b  30965  cdlemg33a  30968  cdlemg33  30973  ltrnco  30981  cdlemg44  30995  cdlemg47  30998  tendococl  31034  tendoplcl  31043  cdlemh1  31077  cdlemh2  31078  cdlemh  31079  cdlemi  31082  cdlemk5  31098  cdlemk6  31099  cdlemksel  31107  cdlemksv2  31109  cdlemk7  31110  cdlemk11  31111  cdlemk12  31112  cdlemkole  31115  cdlemk14  31116  cdlemk15  31117  cdlemk16a  31118  cdlemk16  31119  cdlemk1u  31121  cdlemk5u  31123  cdlemk6u  31124  cdlemkuel  31127  cdlemkuv2  31129  cdlemk18  31130  cdlemk19  31131  cdlemk7u  31132  cdlemk11u  31133  cdlemk12u  31134  cdlemk21N  31135  cdlemk20  31136  cdlemkoatnle-2N  31137  cdlemk13-2N  31138  cdlemkole-2N  31139  cdlemk14-2N  31140  cdlemk15-2N  31141  cdlemk16-2N  31142  cdlemk17-2N  31143  cdlemk18-2N  31148  cdlemk19-2N  31149  cdlemk7u-2N  31150  cdlemk11u-2N  31151  cdlemk12u-2N  31152  cdlemk21-2N  31153  cdlemk20-2N  31154  cdlemkuel-3  31160  cdlemkuv2-3N  31161  cdlemk22-3  31163  cdlemk33N  31171  cdlemk47  31211  cdlemk48  31212  cdlemk49  31213  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk53a  31217  cdlemk55b  31222  cdlemkyyN  31224  cdlemk55u1  31227  cdlemk39u1  31229  cdlemk56  31233  dihord1  31481  dihord2a  31482  dihord10  31486  dihord11c  31487  dihord4  31521  dihord5apre  31525  dihglblem2N  31557  dihglbcpreN  31563  dihmeetlem3N  31568  dihjatc1  31574  dihjatc2N  31575  dihjatc3  31576  mapdpglem24  31967  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmap14lem11  32144  hdmap14lem12  32145  hdmapglem7  32195
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator