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

Theorem simp11 987
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp11  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )

Proof of Theorem simp11
StepHypRef Expression
1 simp1 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl11  1032  simpr11  1041  simp111  1086  simp211  1095  simp311  1104  omeulem1  6817  omeu  6820  ackbij1lem16  8107  coprimeprodsq  13175  pythagtriplem14  13194  pythagtrip  13200  mrelatglb  14602  subglsm  15297  lsmpropd  15301  isfil2  17880  filuni  17909  cxple2a  20582  isosctr  20657  gxdi  21876  measres  24568  bayesth  24689  brbtwn2  25836  colinearalg  25841  ax5seglem3  25862  ofscom  25933  btwndiff  25953  ifscgr  25970  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem4  26016  btwnconn1lem5  26017  btwnconn1lem6  26018  btwnconn1lem7  26019  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem10  26022  btwnconn1lem11  26023  btwnconn1lem12  26024  seglecgr12im  26036  seglecgr12  26037  ivthALT  26319  monotuz  26985  congmul  27013  congsub  27016  rpnnen3lem  27083  eqlkr  29824  lkrshp  29830  lshpkrlem5  29839  cvrval3  30137  4noncolr3  30177  4noncolr2  30178  4noncolr1  30179  athgt  30180  3dimlem2  30183  3dimlem3a  30184  3dimlem4a  30187  3dimlem4  30188  3dimlem4OLDN  30189  3dim2  30192  1cvratex  30197  hlatexch4  30205  ps-2b  30206  3atlem1  30207  3atlem2  30208  3atlem4  30210  3atlem5  30211  3atlem6  30212  llnnleat  30237  2atm  30251  ps-2c  30252  llnmlplnN  30263  lplnnlelln  30267  2atmat  30285  2llnjN  30291  lvoli2  30305  lvolnlelln  30308  4atlem3b  30322  4atlem9  30327  4atlem10a  30328  4atlem10  30330  4atlem11a  30331  4atlem11b  30332  4atlem12a  30334  4atlem12b  30335  4at  30337  4at2  30338  lplncvrlvol2  30339  2lplnj  30344  dalemswapyz  30380  dath2  30461  lneq2at  30502  2lnat  30508  cdlema1N  30515  cdlemb  30518  paddasslem15  30558  pmodlem1  30570  llnmod2i2  30587  llnexchb2lem  30592  llnexchb2  30593  dalawlem1  30595  dalawlem3  30597  dalawlem4  30598  dalawlem5  30599  dalawlem6  30600  dalawlem7  30601  dalawlem8  30602  dalawlem9  30603  dalawlem10  30604  dalawlem11  30605  dalawlem12  30606  dalawlem13  30607  dalawlem15  30609  dalaw  30610  osumcllem5N  30684  osumcllem6N  30685  osumcllem7N  30686  osumcllem9N  30688  osumcllem10N  30689  osumcllem11N  30690  pl42lem1N  30703  lhpexle3lem  30735  lhpmcvr5N  30751  lhp2atne  30758  lhp2at0ne  30760  4atexlemswapqr  30787  4atexlemex6  30798  ldilco  30840  ltrneq  30873  trlval2  30887  trlnidat  30897  cdlemd2  30923  cdlemd7  30928  cdlemd8  30929  cdleme7aa  30966  cdleme7c  30969  cdleme7d  30970  cdleme7e  30971  cdleme7ga  30972  cdleme7  30973  cdleme11c  30985  cdleme11e  30987  cdleme11l  30993  cdleme11  30994  cdleme14  30997  cdleme15a  30998  cdleme15c  31000  cdleme16b  31003  cdleme16c  31004  cdleme16d  31005  cdleme16e  31006  cdleme16f  31007  cdleme0nex  31014  cdleme18d  31019  cdleme19b  31028  cdleme19d  31030  cdleme19e  31031  cdleme20f  31038  cdleme20i  31041  cdleme20k  31043  cdleme20l1  31044  cdleme20l2  31045  cdleme20l  31046  cdleme20m  31047  cdleme21a  31049  cdleme21b  31050  cdleme21ct  31053  cdleme21d  31054  cdleme21e  31055  cdleme21f  31056  cdleme21h  31058  cdleme22eALTN  31069  cdleme22f2  31071  cdleme22g  31072  cdleme26e  31083  cdleme26eALTN  31085  cdleme26fALTN  31086  cdleme26f  31087  cdleme26f2ALTN  31088  cdleme26f2  31089  cdleme28a  31094  cdleme28b  31095  cdleme28  31097  cdleme29ex  31098  cdleme29c  31100  cdlemefrs29cpre1  31122  cdlemefr29exN  31126  cdlemefr32sn2aw  31128  cdlemefr29bpre0N  31130  cdlemefr29clN  31131  cdlemefr32fvaN  31133  cdlemefr32fva1  31134  cdlemefs32sn1aw  31138  cdleme43fsv1snlem  31144  cdleme41sn3a  31157  cdleme32fva  31161  cdleme32b  31166  cdleme32d  31168  cdleme32e  31169  cdleme32f  31170  cdleme32le  31171  cdleme35a  31172  cdleme35fnpq  31173  cdleme35b  31174  cdleme35c  31175  cdleme35d  31176  cdleme35e  31177  cdleme35f  31178  cdleme36a  31184  cdleme36m  31185  cdleme37m  31186  cdleme39a  31189  cdleme39n  31190  cdleme40m  31191  cdleme40n  31192  cdleme42e  31203  cdleme42f  31204  cdleme42g  31205  cdleme43bN  31214  cdleme43cN  31215  cdleme43dN  31216  cdleme46f2g2  31217  cdleme46f2g1  31218  cdleme17d2  31219  cdleme48b  31227  cdleme4gfv  31231  cdlemeg49le  31235  cdlemeg46c  31237  cdlemeg46fvaw  31240  cdlemeg46nlpq  31241  cdlemeg46frv  31249  cdlemeg46rgv  31252  cdlemeg46req  31253  cdlemeg46gfre  31256  cdleme50trn1  31273  cdleme50trn2a  31274  cdleme50trn2  31275  cdleme  31284  cdlemf  31287  trlord  31293  cdlemg2ce  31316  cdlemg7fvbwN  31331  cdlemg7aN  31349  cdlemg10bALTN  31360  cdlemg10a  31364  cdlemg10  31365  cdlemg12d  31370  cdlemg12f  31372  cdlemg12g  31373  cdlemg12  31374  cdlemg13a  31375  cdlemg13  31376  cdlemg17b  31386  cdlemg17dN  31387  cdlemg17dALTN  31388  cdlemg17e  31389  cdlemg17f  31390  cdlemg17g  31391  cdlemg17h  31392  cdlemg17i  31393  cdlemg17pq  31396  cdlemg17bq  31397  cdlemg17iqN  31398  cdlemg17  31401  cdlemg18d  31405  cdlemg18  31406  cdlemg19a  31407  cdlemg19  31408  cdlemg21  31410  cdlemg27a  31416  cdlemg28a  31417  cdlemg31b0N  31418  cdlemg27b  31420  cdlemg33b0  31425  cdlemg28b  31427  cdlemg28  31428  cdlemg33a  31430  cdlemg33  31435  cdlemg34  31436  cdlemg35  31437  cdlemg36  31438  ltrnco  31443  trlcone  31452  cdlemg44  31457  cdlemg47  31460  cdlemg48  31461  tendococl  31496  tendoplcl  31505  cdlemh1  31539  cdlemi  31544  cdlemj1  31545  cdlemj2  31546  tendocan  31548  cdlemk6  31561  cdlemki  31565  cdlemksat  31570  cdlemksv2  31571  cdlemk7  31572  cdlemk11  31573  cdlemk12  31574  cdlemkoatnle  31575  cdlemkole  31577  cdlemk14  31578  cdlemk15  31579  cdlemk16a  31580  cdlemk16  31581  cdlemk17  31582  cdlemk1u  31583  cdlemk5u  31585  cdlemk6u  31586  cdlemkuat  31590  cdlemk18  31592  cdlemk19  31593  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  cdlemk22  31617  cdlemk23-3  31626  cdlemk25-3  31628  cdlemk26b-3  31629  cdlemk27-3  31631  cdlemk28-3  31632  cdlemk33N  31633  cdlemk37  31638  cdlemky  31650  cdlemk11ta  31653  cdlemkid3N  31657  cdlemk11tc  31669  cdlemk11t  31670  cdlemk45  31671  cdlemk46  31672  cdlemk47  31673  cdlemk48  31674  cdlemk49  31675  cdlemk50  31676  cdlemk51  31677  cdlemk52  31678  cdlemk55b  31684  cdlemkyyN  31686  cdlemk55u1  31689  cdlemk55u  31690  cdlemk39u1  31691  cdlemk39u  31692  cdlemk56  31695  cdleml3N  31702  cdleml4N  31703  cdlemm10N  31843  dihord1  31943  dihord2a  31944  dihord2b  31945  dihord10  31948  dihord11c  31949  dihord2pre  31950  dihord4  31983  dihord5apre  31987  dihmeetlem1N  32015  dihglbcpreN  32025  dihjatc1  32036  dihjatc3  32038  dihmeetlem13N  32044  dihmeetlem20N  32051  baerlem3lem2  32435  baerlem5alem2  32436  baerlem5blem2  32437  hdmap14lem11  32606  hdmap14lem12  32607
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