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

Theorem simp11 985
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 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl11  1030  simpr11  1039  simp111  1084  simp211  1093  simp311  1102  omeulem1  6582  omeu  6585  ackbij1lem16  7863  coprimeprodsq  12864  pythagtriplem14  12883  pythagtrip  12889  mrelatglb  14289  subglsm  14984  lsmpropd  14988  isfil2  17553  filuni  17582  cxple2a  20048  isosctr  20123  gxdi  20965  measres  23551  bayesth  23644  brbtwn2  24535  colinearalg  24540  ax5seglem3  24561  ofscom  24632  btwndiff  24652  ifscgr  24669  brofs2  24702  brifs2  24703  fscgr  24705  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem5  24716  btwnconn1lem6  24717  btwnconn1lem7  24718  btwnconn1lem8  24719  btwnconn1lem9  24720  btwnconn1lem10  24721  btwnconn1lem11  24722  btwnconn1lem12  24723  seglecgr12im  24735  seglecgr12  24736  svli2  25495  islimrs3  25592  islimrs4  25593  isibg1a6  26136  ivthALT  26269  monotuz  27037  congmul  27065  congsub  27068  rpnnen3lem  27135  eqlkr  29362  lkrshp  29368  lshpkrlem5  29377  cvrval3  29675  4noncolr3  29715  4noncolr2  29716  4noncolr1  29717  athgt  29718  3dimlem2  29721  3dimlem3a  29722  3dimlem4a  29725  3dimlem4  29726  3dimlem4OLDN  29727  3dim2  29730  1cvratex  29735  hlatexch4  29743  ps-2b  29744  3atlem1  29745  3atlem2  29746  3atlem4  29748  3atlem5  29749  3atlem6  29750  llnnleat  29775  2atm  29789  ps-2c  29790  llnmlplnN  29801  lplnnlelln  29805  2atmat  29823  2llnjN  29829  lvoli2  29843  lvolnlelln  29846  4atlem3b  29860  4atlem9  29865  4atlem10a  29866  4atlem10  29868  4atlem11a  29869  4atlem11b  29870  4atlem12a  29872  4atlem12b  29873  4at  29875  4at2  29876  lplncvrlvol2  29877  2lplnj  29882  dalemswapyz  29918  dath2  29999  lneq2at  30040  2lnat  30046  cdlema1N  30053  cdlemb  30056  paddasslem15  30096  pmodlem1  30108  llnmod2i2  30125  llnexchb2lem  30130  llnexchb2  30131  dalawlem1  30133  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem9  30141  dalawlem10  30142  dalawlem11  30143  dalawlem12  30144  dalawlem13  30145  dalawlem15  30147  dalaw  30148  osumcllem5N  30222  osumcllem6N  30223  osumcllem7N  30224  osumcllem9N  30226  osumcllem10N  30227  osumcllem11N  30228  pl42lem1N  30241  lhpexle3lem  30273  lhpmcvr5N  30289  lhp2atne  30296  lhp2at0ne  30298  4atexlemswapqr  30325  4atexlemex6  30336  ldilco  30378  ltrneq  30411  trlval2  30425  trlnidat  30435  cdlemd2  30461  cdlemd7  30466  cdlemd8  30467  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme11c  30523  cdleme11e  30525  cdleme11l  30531  cdleme11  30532  cdleme14  30535  cdleme15a  30536  cdleme15c  30538  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme0nex  30552  cdleme18d  30557  cdleme19b  30566  cdleme19d  30568  cdleme19e  30569  cdleme20f  30576  cdleme20i  30579  cdleme20k  30581  cdleme20l1  30582  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21a  30587  cdleme21b  30588  cdleme21ct  30591  cdleme21d  30592  cdleme21e  30593  cdleme21f  30594  cdleme21h  30596  cdleme22eALTN  30607  cdleme22f2  30609  cdleme22g  30610  cdleme26e  30621  cdleme26eALTN  30623  cdleme26fALTN  30624  cdleme26f  30625  cdleme26f2ALTN  30626  cdleme26f2  30627  cdleme28a  30632  cdleme28b  30633  cdleme28  30635  cdleme29ex  30636  cdleme29c  30638  cdlemefrs29cpre1  30660  cdlemefr29exN  30664  cdlemefr32sn2aw  30666  cdlemefr29bpre0N  30668  cdlemefr29clN  30669  cdlemefr32fvaN  30671  cdlemefr32fva1  30672  cdlemefs32sn1aw  30676  cdleme43fsv1snlem  30682  cdleme41sn3a  30695  cdleme32fva  30699  cdleme32b  30704  cdleme32d  30706  cdleme32e  30707  cdleme32f  30708  cdleme32le  30709  cdleme35a  30710  cdleme35fnpq  30711  cdleme35b  30712  cdleme35c  30713  cdleme35d  30714  cdleme35e  30715  cdleme35f  30716  cdleme36a  30722  cdleme36m  30723  cdleme37m  30724  cdleme39a  30727  cdleme39n  30728  cdleme40m  30729  cdleme40n  30730  cdleme42e  30741  cdleme42f  30742  cdleme42g  30743  cdleme43bN  30752  cdleme43cN  30753  cdleme43dN  30754  cdleme46f2g2  30755  cdleme46f2g1  30756  cdleme17d2  30757  cdleme48b  30765  cdleme4gfv  30769  cdlemeg49le  30773  cdlemeg46c  30775  cdlemeg46fvaw  30778  cdlemeg46nlpq  30779  cdlemeg46frv  30787  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfre  30794  cdleme50trn1  30811  cdleme50trn2a  30812  cdleme50trn2  30813  cdleme  30822  cdlemf  30825  trlord  30831  cdlemg2ce  30854  cdlemg7fvbwN  30869  cdlemg7aN  30887  cdlemg10bALTN  30898  cdlemg10a  30902  cdlemg10  30903  cdlemg12d  30908  cdlemg12f  30910  cdlemg12g  30911  cdlemg12  30912  cdlemg13a  30913  cdlemg13  30914  cdlemg17b  30924  cdlemg17dN  30925  cdlemg17dALTN  30926  cdlemg17e  30927  cdlemg17f  30928  cdlemg17g  30929  cdlemg17h  30930  cdlemg17i  30931  cdlemg17pq  30934  cdlemg17bq  30935  cdlemg17iqN  30936  cdlemg17  30939  cdlemg18d  30943  cdlemg18  30944  cdlemg19a  30945  cdlemg19  30946  cdlemg21  30948  cdlemg27a  30954  cdlemg28a  30955  cdlemg31b0N  30956  cdlemg27b  30958  cdlemg33b0  30963  cdlemg28b  30965  cdlemg28  30966  cdlemg33a  30968  cdlemg33  30973  cdlemg34  30974  cdlemg35  30975  cdlemg36  30976  ltrnco  30981  trlcone  30990  cdlemg44  30995  cdlemg47  30998  cdlemg48  30999  tendococl  31034  tendoplcl  31043  cdlemh1  31077  cdlemi  31082  cdlemj1  31083  cdlemj2  31084  tendocan  31086  cdlemk6  31099  cdlemki  31103  cdlemksat  31108  cdlemksv2  31109  cdlemk7  31110  cdlemk11  31111  cdlemk12  31112  cdlemkoatnle  31113  cdlemkole  31115  cdlemk14  31116  cdlemk15  31117  cdlemk16a  31118  cdlemk16  31119  cdlemk17  31120  cdlemk1u  31121  cdlemk5u  31123  cdlemk6u  31124  cdlemkuat  31128  cdlemk18  31130  cdlemk19  31131  cdlemk12u  31134  cdlemk21N  31135  cdlemk20  31136  cdlemkoatnle-2N  31137  cdlemk13-2N  31138  cdlemkole-2N  31139  cdlemk14-2N  31140  cdlemk15-2N  31141  cdlemk16-2N  31142  cdlemk17-2N  31143  cdlemk18-2N  31148  cdlemk19-2N  31149  cdlemk7u-2N  31150  cdlemk11u-2N  31151  cdlemk12u-2N  31152  cdlemk21-2N  31153  cdlemk20-2N  31154  cdlemk22  31155  cdlemk23-3  31164  cdlemk25-3  31166  cdlemk26b-3  31167  cdlemk27-3  31169  cdlemk28-3  31170  cdlemk33N  31171  cdlemk37  31176  cdlemky  31188  cdlemk11ta  31191  cdlemkid3N  31195  cdlemk11tc  31207  cdlemk11t  31208  cdlemk45  31209  cdlemk46  31210  cdlemk47  31211  cdlemk48  31212  cdlemk49  31213  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk55b  31222  cdlemkyyN  31224  cdlemk55u1  31227  cdlemk55u  31228  cdlemk39u1  31229  cdlemk39u  31230  cdlemk56  31233  cdleml3N  31240  cdleml4N  31241  cdlemm10N  31381  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord10  31486  dihord11c  31487  dihord2pre  31488  dihord4  31521  dihord5apre  31525  dihmeetlem1N  31553  dihglbcpreN  31563  dihjatc1  31574  dihjatc3  31576  dihmeetlem13N  31582  dihmeetlem20N  31589  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmap14lem11  32144  hdmap14lem12  32145
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