MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11 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  6754  omeu  6757  ackbij1lem16  8041  coprimeprodsq  13103  pythagtriplem14  13122  pythagtrip  13128  mrelatglb  14530  subglsm  15225  lsmpropd  15229  isfil2  17802  filuni  17831  cxple2a  20450  isosctr  20525  gxdi  21725  measres  24363  bayesth  24469  brbtwn2  25551  colinearalg  25556  ax5seglem3  25577  ofscom  25648  btwndiff  25668  ifscgr  25685  brofs2  25718  brifs2  25719  fscgr  25721  btwnconn1lem1  25728  btwnconn1lem2  25729  btwnconn1lem3  25730  btwnconn1lem4  25731  btwnconn1lem5  25732  btwnconn1lem6  25733  btwnconn1lem7  25734  btwnconn1lem8  25735  btwnconn1lem9  25736  btwnconn1lem10  25737  btwnconn1lem11  25738  btwnconn1lem12  25739  seglecgr12im  25751  seglecgr12  25752  ivthALT  26022  monotuz  26688  congmul  26716  congsub  26719  rpnnen3lem  26786  eqlkr  29265  lkrshp  29271  lshpkrlem5  29280  cvrval3  29578  4noncolr3  29618  4noncolr2  29619  4noncolr1  29620  athgt  29621  3dimlem2  29624  3dimlem3a  29625  3dimlem4a  29628  3dimlem4  29629  3dimlem4OLDN  29630  3dim2  29633  1cvratex  29638  hlatexch4  29646  ps-2b  29647  3atlem1  29648  3atlem2  29649  3atlem4  29651  3atlem5  29652  3atlem6  29653  llnnleat  29678  2atm  29692  ps-2c  29693  llnmlplnN  29704  lplnnlelln  29708  2atmat  29726  2llnjN  29732  lvoli2  29746  lvolnlelln  29749  4atlem3b  29763  4atlem9  29768  4atlem10a  29769  4atlem10  29771  4atlem11a  29772  4atlem11b  29773  4atlem12a  29775  4atlem12b  29776  4at  29778  4at2  29779  lplncvrlvol2  29780  2lplnj  29785  dalemswapyz  29821  dath2  29902  lneq2at  29943  2lnat  29949  cdlema1N  29956  cdlemb  29959  paddasslem15  29999  pmodlem1  30011  llnmod2i2  30028  llnexchb2lem  30033  llnexchb2  30034  dalawlem1  30036  dalawlem3  30038  dalawlem4  30039  dalawlem5  30040  dalawlem6  30041  dalawlem7  30042  dalawlem8  30043  dalawlem9  30044  dalawlem10  30045  dalawlem11  30046  dalawlem12  30047  dalawlem13  30048  dalawlem15  30050  dalaw  30051  osumcllem5N  30125  osumcllem6N  30126  osumcllem7N  30127  osumcllem9N  30129  osumcllem10N  30130  osumcllem11N  30131  pl42lem1N  30144  lhpexle3lem  30176  lhpmcvr5N  30192  lhp2atne  30199  lhp2at0ne  30201  4atexlemswapqr  30228  4atexlemex6  30239  ldilco  30281  ltrneq  30314  trlval2  30328  trlnidat  30338  cdlemd2  30364  cdlemd7  30369  cdlemd8  30370  cdleme7aa  30407  cdleme7c  30410  cdleme7d  30411  cdleme7e  30412  cdleme7ga  30413  cdleme7  30414  cdleme11c  30426  cdleme11e  30428  cdleme11l  30434  cdleme11  30435  cdleme14  30438  cdleme15a  30439  cdleme15c  30441  cdleme16b  30444  cdleme16c  30445  cdleme16d  30446  cdleme16e  30447  cdleme16f  30448  cdleme0nex  30455  cdleme18d  30460  cdleme19b  30469  cdleme19d  30471  cdleme19e  30472  cdleme20f  30479  cdleme20i  30482  cdleme20k  30484  cdleme20l1  30485  cdleme20l2  30486  cdleme20l  30487  cdleme20m  30488  cdleme21a  30490  cdleme21b  30491  cdleme21ct  30494  cdleme21d  30495  cdleme21e  30496  cdleme21f  30497  cdleme21h  30499  cdleme22eALTN  30510  cdleme22f2  30512  cdleme22g  30513  cdleme26e  30524  cdleme26eALTN  30526  cdleme26fALTN  30527  cdleme26f  30528  cdleme26f2ALTN  30529  cdleme26f2  30530  cdleme28a  30535  cdleme28b  30536  cdleme28  30538  cdleme29ex  30539  cdleme29c  30541  cdlemefrs29cpre1  30563  cdlemefr29exN  30567  cdlemefr32sn2aw  30569  cdlemefr29bpre0N  30571  cdlemefr29clN  30572  cdlemefr32fvaN  30574  cdlemefr32fva1  30575  cdlemefs32sn1aw  30579  cdleme43fsv1snlem  30585  cdleme41sn3a  30598  cdleme32fva  30602  cdleme32b  30607  cdleme32d  30609  cdleme32e  30610  cdleme32f  30611  cdleme32le  30612  cdleme35a  30613  cdleme35fnpq  30614  cdleme35b  30615  cdleme35c  30616  cdleme35d  30617  cdleme35e  30618  cdleme35f  30619  cdleme36a  30625  cdleme36m  30626  cdleme37m  30627  cdleme39a  30630  cdleme39n  30631  cdleme40m  30632  cdleme40n  30633  cdleme42e  30644  cdleme42f  30645  cdleme42g  30646  cdleme43bN  30655  cdleme43cN  30656  cdleme43dN  30657  cdleme46f2g2  30658  cdleme46f2g1  30659  cdleme17d2  30660  cdleme48b  30668  cdleme4gfv  30672  cdlemeg49le  30676  cdlemeg46c  30678  cdlemeg46fvaw  30681  cdlemeg46nlpq  30682  cdlemeg46frv  30690  cdlemeg46rgv  30693  cdlemeg46req  30694  cdlemeg46gfre  30697  cdleme50trn1  30714  cdleme50trn2a  30715  cdleme50trn2  30716  cdleme  30725  cdlemf  30728  trlord  30734  cdlemg2ce  30757  cdlemg7fvbwN  30772  cdlemg7aN  30790  cdlemg10bALTN  30801  cdlemg10a  30805  cdlemg10  30806  cdlemg12d  30811  cdlemg12f  30813  cdlemg12g  30814  cdlemg12  30815  cdlemg13a  30816  cdlemg13  30817  cdlemg17b  30827  cdlemg17dN  30828  cdlemg17dALTN  30829  cdlemg17e  30830  cdlemg17f  30831  cdlemg17g  30832  cdlemg17h  30833  cdlemg17i  30834  cdlemg17pq  30837  cdlemg17bq  30838  cdlemg17iqN  30839  cdlemg17  30842  cdlemg18d  30846  cdlemg18  30847  cdlemg19a  30848  cdlemg19  30849  cdlemg21  30851  cdlemg27a  30857  cdlemg28a  30858  cdlemg31b0N  30859  cdlemg27b  30861  cdlemg33b0  30866  cdlemg28b  30868  cdlemg28  30869  cdlemg33a  30871  cdlemg33  30876  cdlemg34  30877  cdlemg35  30878  cdlemg36  30879  ltrnco  30884  trlcone  30893  cdlemg44  30898  cdlemg47  30901  cdlemg48  30902  tendococl  30937  tendoplcl  30946  cdlemh1  30980  cdlemi  30985  cdlemj1  30986  cdlemj2  30987  tendocan  30989  cdlemk6  31002  cdlemki  31006  cdlemksat  31011  cdlemksv2  31012  cdlemk7  31013  cdlemk11  31014  cdlemk12  31015  cdlemkoatnle  31016  cdlemkole  31018  cdlemk14  31019  cdlemk15  31020  cdlemk16a  31021  cdlemk16  31022  cdlemk17  31023  cdlemk1u  31024  cdlemk5u  31026  cdlemk6u  31027  cdlemkuat  31031  cdlemk18  31033  cdlemk19  31034  cdlemk12u  31037  cdlemk21N  31038  cdlemk20  31039  cdlemkoatnle-2N  31040  cdlemk13-2N  31041  cdlemkole-2N  31042  cdlemk14-2N  31043  cdlemk15-2N  31044  cdlemk16-2N  31045  cdlemk17-2N  31046  cdlemk18-2N  31051  cdlemk19-2N  31052  cdlemk7u-2N  31053  cdlemk11u-2N  31054  cdlemk12u-2N  31055  cdlemk21-2N  31056  cdlemk20-2N  31057  cdlemk22  31058  cdlemk23-3  31067  cdlemk25-3  31069  cdlemk26b-3  31070  cdlemk27-3  31072  cdlemk28-3  31073  cdlemk33N  31074  cdlemk37  31079  cdlemky  31091  cdlemk11ta  31094  cdlemkid3N  31098  cdlemk11tc  31110  cdlemk11t  31111  cdlemk45  31112  cdlemk46  31113  cdlemk47  31114  cdlemk48  31115  cdlemk49  31116  cdlemk50  31117  cdlemk51  31118  cdlemk52  31119  cdlemk55b  31125  cdlemkyyN  31127  cdlemk55u1  31130  cdlemk55u  31131  cdlemk39u1  31132  cdlemk39u  31133  cdlemk56  31136  cdleml3N  31143  cdleml4N  31144  cdlemm10N  31284  dihord1  31384  dihord2a  31385  dihord2b  31386  dihord10  31389  dihord11c  31390  dihord2pre  31391  dihord4  31424  dihord5apre  31428  dihmeetlem1N  31456  dihglbcpreN  31466  dihjatc1  31477  dihjatc3  31479  dihmeetlem13N  31485  dihmeetlem20N  31492  baerlem3lem2  31876  baerlem5alem2  31877  baerlem5blem2  31878  hdmap14lem11  32047  hdmap14lem12  32048
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