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  6599  ackbij1lem16  7877  dvdsgcd  12738  coprimeprodsq  12878  pythagtriplem4  12888  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  pythagtrip  12903  lsmpropd  15002  isfil2  17567  filuni  17596  ufprim  17620  cxple2a  20062  isosctr  20137  measres  23564  bayesth  23657  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axcontlem4  24667  ofscom  24702  btwndiff  24722  ifscgr  24739  brofs2  24772  brifs2  24773  fscgr  24775  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem12  24793  seglecgr12im  24805  seglecgr12  24806  intcont  25646  islimrs3  25684  islimrs4  25685  isibg1a6  26228  ivthALT  26361  mzpsubst  26929  congmul  27157  congsub  27160  islshpcv  29865  eqlkr  29911  lshpsmreu  29921  lshpkrlem5  29926  atlrelat1  30133  cvlcvr1  30151  cvlcvrp  30152  cvlatcvr1  30153  cvlatcvr2  30154  4noncolr3  30264  4noncolr2  30265  4noncolr1  30266  athgt  30267  3dimlem2  30270  3dimlem3a  30271  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  3dim1  30278  3dim2  30279  hlatexch4  30292  ps-2b  30293  3atlem6  30299  llnnleat  30324  2atm  30338  ps-2c  30339  llnmlplnN  30350  2atmat  30372  2llnjN  30378  lvoli2  30392  4atlem3b  30409  4atlem10  30417  4atlem11a  30418  4atlem11b  30419  4atlem12a  30421  4atlem12b  30422  dalemswapyz  30467  lneq2at  30589  2lnat  30595  cdlema1N  30602  cdlemb  30605  pmodlem1  30657  llnmod2i2  30674  dalawlem1  30682  dalawlem3  30684  dalawlem4  30685  dalawlem6  30687  dalawlem9  30690  dalawlem10  30691  dalawlem11  30692  dalawlem12  30693  dalawlem13  30694  dalawlem15  30696  dalaw  30697  pclfinN  30711  osumcllem5N  30771  osumcllem6N  30772  osumcllem7N  30773  osumcllem9N  30775  osumcllem11N  30777  pl42lem1N  30790  lhp2at0  30843  lhp2atne  30845  lhp2at0ne  30847  4atexlem7  30886  ldilco  30927  ltrneq  30960  cdlemd2  31010  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7ga  31059  cdleme11c  31072  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme0nex  31101  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20f  31125  cdleme20k  31130  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme21f  31143  cdleme21i  31146  cdleme22cN  31153  cdleme22eALTN  31156  cdleme25a  31164  cdleme25c  31166  cdleme25dN  31167  cdleme26e  31170  cdleme26ee  31171  cdleme26eALTN  31172  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme28a  31181  cdleme28b  31182  cdleme28  31184  cdlemefr32sn2aw  31215  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32c  31254  cdleme32e  31256  cdleme32le  31258  cdleme35a  31259  cdleme35b  31261  cdleme35d  31263  cdleme36a  31271  cdleme36m  31272  cdleme39a  31276  cdleme40m  31278  cdleme40n  31279  cdleme43bN  31301  cdleme43dN  31303  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme4gfv  31318  cdlemeg49le  31322  cdlemeg46c  31324  cdlemeg46fvaw  31327  cdlemeg46nlpq  31328  cdlemeg46gfre  31343  cdleme50trn2  31362  cdlemg2ce  31403  cdlemg2idN  31407  cdlemg7fvbwN  31418  cdlemg10bALTN  31447  cdlemg10a  31451  cdlemg12d  31457  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg17b  31473  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17pq  31483  cdlemg17bq  31484  cdlemg18d  31492  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg31b0N  31505  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33c0  31513  cdlemg28b  31514  cdlemg33a  31517  cdlemg33  31522  ltrnco  31530  cdlemg44  31544  cdlemg47  31547  tendococl  31583  tendoplcl  31592  cdlemh1  31626  cdlemh2  31627  cdlemh  31628  cdlemi  31631  cdlemk5  31647  cdlemk6  31648  cdlemksel  31656  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk1u  31670  cdlemk5u  31672  cdlemk6u  31673  cdlemkuel  31676  cdlemkuv2  31678  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk21-2N  31702  cdlemk20-2N  31703  cdlemkuel-3  31709  cdlemkuv2-3N  31710  cdlemk22-3  31712  cdlemk33N  31720  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk55b  31771  cdlemkyyN  31773  cdlemk55u1  31776  cdlemk39u1  31778  cdlemk56  31782  dihord1  32030  dihord2a  32031  dihord10  32035  dihord11c  32036  dihord4  32070  dihord5apre  32074  dihglblem2N  32106  dihglbcpreN  32112  dihmeetlem3N  32117  dihjatc1  32123  dihjatc2N  32124  dihjatc3  32125  mapdpglem24  32516  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmap14lem11  32693  hdmap14lem12  32694  hdmapglem7  32744
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