MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp13 Structured version   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  5493  omeu  6820  ackbij1lem16  8107  dvdsgcd  13035  coprimeprodsq  13175  pythagtriplem4  13185  pythagtriplem13  13193  pythagtriplem14  13194  pythagtriplem16  13196  pythagtrip  13200  lsmpropd  15301  isfil2  17880  filuni  17909  ufprim  17933  cxple2a  20582  isosctr  20657  measres  24568  bayesth  24689  brbtwn2  25836  colinearalg  25841  ax5seg  25869  axcontlem4  25898  ofscom  25933  btwndiff  25953  ifscgr  25970  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem12  26024  seglecgr12im  26036  seglecgr12  26037  ivthALT  26319  mzpsubst  26786  congmul  27013  congsub  27016  islshpcv  29778  eqlkr  29824  lshpsmreu  29834  lshpkrlem5  29839  atlrelat1  30046  cvlcvr1  30064  cvlcvrp  30065  cvlatcvr1  30066  cvlatcvr2  30067  4noncolr3  30177  4noncolr2  30178  4noncolr1  30179  athgt  30180  3dimlem2  30183  3dimlem3a  30184  3dimlem4a  30187  3dimlem4  30188  3dimlem4OLDN  30189  3dim1  30191  3dim2  30192  hlatexch4  30205  ps-2b  30206  3atlem6  30212  llnnleat  30237  2atm  30251  ps-2c  30252  llnmlplnN  30263  2atmat  30285  2llnjN  30291  lvoli2  30305  4atlem3b  30322  4atlem10  30330  4atlem11a  30331  4atlem11b  30332  4atlem12a  30334  4atlem12b  30335  dalemswapyz  30380  lneq2at  30502  2lnat  30508  cdlema1N  30515  cdlemb  30518  pmodlem1  30570  llnmod2i2  30587  dalawlem1  30595  dalawlem3  30597  dalawlem4  30598  dalawlem6  30600  dalawlem9  30603  dalawlem10  30604  dalawlem11  30605  dalawlem12  30606  dalawlem13  30607  dalawlem15  30609  dalaw  30610  pclfinN  30624  osumcllem5N  30684  osumcllem6N  30685  osumcllem7N  30686  osumcllem9N  30688  osumcllem11N  30690  pl42lem1N  30703  lhp2at0  30756  lhp2atne  30758  lhp2at0ne  30760  4atexlem7  30799  ldilco  30840  ltrneq  30873  cdlemd2  30923  cdleme0ex2N  30948  cdleme7aa  30966  cdleme7c  30969  cdleme7d  30970  cdleme7ga  30972  cdleme11c  30985  cdleme11l  30993  cdleme11  30994  cdleme14  30997  cdleme15a  30998  cdleme15c  31000  cdleme16b  31003  cdleme16c  31004  cdleme16d  31005  cdleme16e  31006  cdleme16f  31007  cdleme0nex  31014  cdleme19b  31028  cdleme19d  31030  cdleme19e  31031  cdleme20f  31038  cdleme20k  31043  cdleme20l1  31044  cdleme20l2  31045  cdleme20l  31046  cdleme20m  31047  cdleme21a  31049  cdleme21b  31050  cdleme21c  31051  cdleme21ct  31053  cdleme21d  31054  cdleme21e  31055  cdleme21f  31056  cdleme21i  31059  cdleme22cN  31066  cdleme22eALTN  31069  cdleme25a  31077  cdleme25c  31079  cdleme25dN  31080  cdleme26e  31083  cdleme26ee  31084  cdleme26eALTN  31085  cdleme26f2ALTN  31088  cdleme26f2  31089  cdleme28a  31094  cdleme28b  31095  cdleme28  31097  cdlemefr32sn2aw  31128  cdlemefs32sn1aw  31138  cdleme43fsv1snlem  31144  cdleme41sn3a  31157  cdleme32c  31167  cdleme32e  31169  cdleme32le  31171  cdleme35a  31172  cdleme35b  31174  cdleme35d  31176  cdleme36a  31184  cdleme36m  31185  cdleme39a  31189  cdleme40m  31191  cdleme40n  31192  cdleme43bN  31214  cdleme43dN  31216  cdleme46f2g2  31217  cdleme46f2g1  31218  cdleme4gfv  31231  cdlemeg49le  31235  cdlemeg46c  31237  cdlemeg46fvaw  31240  cdlemeg46nlpq  31241  cdlemeg46gfre  31256  cdleme50trn2  31275  cdlemg2ce  31316  cdlemg2idN  31320  cdlemg7fvbwN  31331  cdlemg10bALTN  31360  cdlemg10a  31364  cdlemg12d  31370  cdlemg12g  31373  cdlemg12  31374  cdlemg13a  31375  cdlemg13  31376  cdlemg17b  31386  cdlemg17dN  31387  cdlemg17dALTN  31388  cdlemg17e  31389  cdlemg17pq  31396  cdlemg17bq  31397  cdlemg18d  31405  cdlemg19a  31407  cdlemg19  31408  cdlemg21  31410  cdlemg27a  31416  cdlemg31b0N  31418  cdlemg27b  31420  cdlemg31c  31423  cdlemg33b0  31425  cdlemg33c0  31426  cdlemg28b  31427  cdlemg33a  31430  cdlemg33  31435  ltrnco  31443  cdlemg44  31457  cdlemg47  31460  tendococl  31496  tendoplcl  31505  cdlemh1  31539  cdlemh2  31540  cdlemh  31541  cdlemi  31544  cdlemk5  31560  cdlemk6  31561  cdlemksel  31569  cdlemksv2  31571  cdlemk7  31572  cdlemk11  31573  cdlemk12  31574  cdlemkole  31577  cdlemk14  31578  cdlemk15  31579  cdlemk16a  31580  cdlemk16  31581  cdlemk1u  31583  cdlemk5u  31585  cdlemk6u  31586  cdlemkuel  31589  cdlemkuv2  31591  cdlemk18  31592  cdlemk19  31593  cdlemk7u  31594  cdlemk11u  31595  cdlemk12u  31596  cdlemk21N  31597  cdlemk20  31598  cdlemkoatnle-2N  31599  cdlemk13-2N  31600  cdlemkole-2N  31601  cdlemk14-2N  31602  cdlemk15-2N  31603  cdlemk16-2N  31604  cdlemk17-2N  31605  cdlemk18-2N  31610  cdlemk19-2N  31611  cdlemk7u-2N  31612  cdlemk11u-2N  31613  cdlemk12u-2N  31614  cdlemk21-2N  31615  cdlemk20-2N  31616  cdlemkuel-3  31622  cdlemkuv2-3N  31623  cdlemk22-3  31625  cdlemk33N  31633  cdlemk47  31673  cdlemk48  31674  cdlemk49  31675  cdlemk50  31676  cdlemk51  31677  cdlemk52  31678  cdlemk53a  31679  cdlemk55b  31684  cdlemkyyN  31686  cdlemk55u1  31689  cdlemk39u1  31691  cdlemk56  31695  dihord1  31943  dihord2a  31944  dihord10  31948  dihord11c  31949  dihord4  31983  dihord5apre  31987  dihglblem2N  32019  dihglbcpreN  32025  dihmeetlem3N  32030  dihjatc1  32036  dihjatc2N  32037  dihjatc3  32038  mapdpglem24  32429  baerlem3lem2  32435  baerlem5alem2  32436  baerlem5blem2  32437  hdmap14lem11  32606  hdmap14lem12  32607  hdmapglem7  32657
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