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  6583  ackbij1lem16  7861  dvdsgcd  12722  coprimeprodsq  12862  pythagtriplem4  12872  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pythagtrip  12887  lsmpropd  14986  isfil2  17551  filuni  17580  ufprim  17604  cxple2a  20046  isosctr  20121  measres  23549  bayesth  23642  brbtwn2  24533  colinearalg  24538  ax5seg  24566  axcontlem4  24595  ofscom  24630  btwndiff  24650  ifscgr  24667  brofs2  24700  brifs2  24701  fscgr  24703  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem12  24721  seglecgr12im  24733  seglecgr12  24734  intcont  25543  islimrs3  25581  islimrs4  25582  isibg1a6  26125  ivthALT  26258  mzpsubst  26826  congmul  27054  congsub  27057  islshpcv  29243  eqlkr  29289  lshpsmreu  29299  lshpkrlem5  29304  atlrelat1  29511  cvlcvr1  29529  cvlcvrp  29530  cvlatcvr1  29531  cvlatcvr2  29532  4noncolr3  29642  4noncolr2  29643  4noncolr1  29644  athgt  29645  3dimlem2  29648  3dimlem3a  29649  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  3dim1  29656  3dim2  29657  hlatexch4  29670  ps-2b  29671  3atlem6  29677  llnnleat  29702  2atm  29716  ps-2c  29717  llnmlplnN  29728  2atmat  29750  2llnjN  29756  lvoli2  29770  4atlem3b  29787  4atlem10  29795  4atlem11a  29796  4atlem11b  29797  4atlem12a  29799  4atlem12b  29800  dalemswapyz  29845  lneq2at  29967  2lnat  29973  cdlema1N  29980  cdlemb  29983  pmodlem1  30035  llnmod2i2  30052  dalawlem1  30060  dalawlem3  30062  dalawlem4  30063  dalawlem6  30065  dalawlem9  30068  dalawlem10  30069  dalawlem11  30070  dalawlem12  30071  dalawlem13  30072  dalawlem15  30074  dalaw  30075  pclfinN  30089  osumcllem5N  30149  osumcllem6N  30150  osumcllem7N  30151  osumcllem9N  30153  osumcllem11N  30155  pl42lem1N  30168  lhp2at0  30221  lhp2atne  30223  lhp2at0ne  30225  4atexlem7  30264  ldilco  30305  ltrneq  30338  cdlemd2  30388  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7ga  30437  cdleme11c  30450  cdleme11l  30458  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme0nex  30479  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20f  30503  cdleme20k  30508  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme21f  30521  cdleme21i  30524  cdleme22cN  30531  cdleme22eALTN  30534  cdleme25a  30542  cdleme25c  30544  cdleme25dN  30545  cdleme26e  30548  cdleme26ee  30549  cdleme26eALTN  30550  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme28a  30559  cdleme28b  30560  cdleme28  30562  cdlemefr32sn2aw  30593  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32c  30632  cdleme32e  30634  cdleme32le  30636  cdleme35a  30637  cdleme35b  30639  cdleme35d  30641  cdleme36a  30649  cdleme36m  30650  cdleme39a  30654  cdleme40m  30656  cdleme40n  30657  cdleme43bN  30679  cdleme43dN  30681  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme4gfv  30696  cdlemeg49le  30700  cdlemeg46c  30702  cdlemeg46fvaw  30705  cdlemeg46nlpq  30706  cdlemeg46gfre  30721  cdleme50trn2  30740  cdlemg2ce  30781  cdlemg2idN  30785  cdlemg7fvbwN  30796  cdlemg10bALTN  30825  cdlemg10a  30829  cdlemg12d  30835  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg17b  30851  cdlemg17dN  30852  cdlemg17dALTN  30853  cdlemg17e  30854  cdlemg17pq  30861  cdlemg17bq  30862  cdlemg18d  30870  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg31b0N  30883  cdlemg27b  30885  cdlemg31c  30888  cdlemg33b0  30890  cdlemg33c0  30891  cdlemg28b  30892  cdlemg33a  30895  cdlemg33  30900  ltrnco  30908  cdlemg44  30922  cdlemg47  30925  tendococl  30961  tendoplcl  30970  cdlemh1  31004  cdlemh2  31005  cdlemh  31006  cdlemi  31009  cdlemk5  31025  cdlemk6  31026  cdlemksel  31034  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  cdlemk1u  31048  cdlemk5u  31050  cdlemk6u  31051  cdlemkuel  31054  cdlemkuv2  31056  cdlemk18  31057  cdlemk19  31058  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk21-2N  31080  cdlemk20-2N  31081  cdlemkuel-3  31087  cdlemkuv2-3N  31088  cdlemk22-3  31090  cdlemk33N  31098  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk55b  31149  cdlemkyyN  31151  cdlemk55u1  31154  cdlemk39u1  31156  cdlemk56  31160  dihord1  31408  dihord2a  31409  dihord10  31413  dihord11c  31414  dihord4  31448  dihord5apre  31452  dihglblem2N  31484  dihglbcpreN  31490  dihmeetlem3N  31495  dihjatc1  31501  dihjatc2N  31502  dihjatc3  31503  mapdpglem24  31894  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmap14lem11  32071  hdmap14lem12  32072  hdmapglem7  32122
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