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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 998 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1019 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976
This theorem is referenced by:  simpl22  1076  simpr22  1085  simp122  1130  simp222  1139  simp322  1148  elfiun  7923  cofsmo  8680  modexp  12343  funcoppc  15486  funcres  15507  catcisolem  15707  1stfcl  15788  2ndfcl  15789  prfcl  15794  evlfcl  15813  curf1cl  15819  curfcl  15823  hofcl  15850  mulgdirlem  16488  pmtrprfv3  16801  mdetunilem4  19407  mdetuni0  19413  mdetmul  19415  prdsxmetlem  21161  isosctrlem3  23477  isosctr  23478  amgmlem  23643  f1otrg  24578  colinearalg  24617  ax5seglem6  24641  ax5seg  24645  axpasch  24648  axeuclidlem  24669  axeuclid  24670  ogrpsub  28145  ogrpaddlt  28146  ogrpsublt  28150  rhmdvd  28250  bnj966  29316  mclspps  29783  cgrtr  30317  cgrtr3  30319  ofscom  30332  cgrextend  30333  btwnxfr  30381  colinearxfr  30400  lineext  30401  fscgr  30405  linecgr  30406  btwnconn1lem1  30412  btwnconn1lem2  30413  btwnconn1lem3  30414  btwnconn1lem4  30415  btwnconn1lem5  30416  btwnconn1lem6  30417  btwnconn1lem7  30418  seglecgr12im  30435  seglecgr12  30436  segletr  30439  broutsideof3  30451  outsideofeq  30455  lineunray  30472  linecom  30475  eqlkr  32097  lshpkrlem5  32112  omlmod1i2N  32258  cvrnbtwn3  32274  cvrcmp2  32282  cvlexch2  32327  cvlexchb2  32329  cvlatexchb2  32333  cvlatexch1  32334  cvlatexch2  32335  cvlatexch3  32336  cvlsupr7  32346  cvlsupr8  32347  atnlej1  32376  atnlej2  32377  2llnneN  32406  cvratlem  32418  atcvrneN  32427  atlelt  32435  2atjm  32442  3noncolr2  32446  3noncolr1N  32447  hlatcon2  32449  3dimlem2  32456  3dim1  32464  3dim2  32465  1cvrat  32473  ps-1  32474  ps-2  32475  2atjlej  32476  hlatexch3N  32477  ps-2b  32479  3atlem1  32480  3atlem5  32484  3atlem6  32485  2atm  32524  ps-2c  32525  lplni2  32534  lplnri3N  32552  llncvrlpln2  32554  2atmat  32558  2llnm2N  32565  2llnm3N  32566  2llnm4  32567  2llnmeqat  32568  lvolnle3at  32579  4atlem0ae  32591  4atlem0be  32592  4atlem3b  32595  4atlem9  32600  4atlem10a  32601  4atlem10  32603  4atlem11a  32604  4atlem12a  32607  4at2  32611  2lplnm2N  32618  lneq2at  32775  2llnma1b  32783  2llnma1  32784  2llnma3r  32785  2llnma2  32786  2llnma2rN  32787  cdlema1N  32788  paddasslem2  32818  paddasslem16  32832  pmodlem1  32843  pmod2iN  32846  hlmod1i  32853  atmod2i1  32858  atmod2i2  32859  atmod3i1  32861  atmod3i2  32862  atmod4i1  32863  atmod4i2  32864  llnexchb2lem  32865  llnexch2N  32867  dalawlem3  32870  dalawlem4  32871  dalawlem5  32872  dalawlem6  32873  dalawlem7  32874  dalawlem8  32875  dalawlem9  32876  dalawlem11  32878  dalawlem12  32879  dalawlem13  32880  dalawlem15  32882  osumcllem7N  32959  osumcllem9N  32961  pl42lem1N  32976  4atexlemswapqr  33060  4atex2  33074  4atex2-0bOLDN  33076  trlval4  33186  cdlemc5  33193  cdlemc6  33194  cdlemd2  33197  cdlemd4  33199  cdlemd6  33201  cdleme00a  33207  cdleme0e  33215  cdleme4  33236  cdleme4a  33237  cdleme5  33238  cdleme9  33251  cdleme16aN  33257  cdleme11c  33259  cdleme11dN  33260  cdleme11e  33261  cdleme11g  33263  cdleme11h  33264  cdleme11j  33265  cdleme11k  33266  cdleme11l  33267  cdleme11  33268  cdleme12  33269  cdleme13  33270  cdleme14  33271  cdleme15a  33272  cdleme15c  33274  cdleme16b  33277  cdleme16c  33278  cdleme16d  33279  cdleme16e  33280  cdleme16f  33281  cdleme17d1  33287  cdleme0nex  33288  cdleme18a  33289  cdleme18b  33290  cdleme18c  33291  cdleme18d  33293  cdlemednpq  33297  cdlemednuN  33298  cdleme20zN  33299  cdleme20y  33300  cdleme20yOLD  33301  cdleme19a  33302  cdleme19b  33303  cdleme19d  33305  cdleme19e  33306  cdleme20aN  33308  cdleme20d  33311  cdleme20f  33313  cdleme20g  33314  cdleme20i  33316  cdleme20j  33317  cdleme20l1  33319  cdleme20l2  33320  cdleme20l  33321  cdleme20m  33322  cdleme21b  33325  cdleme21c  33326  cdleme21e  33330  cdleme21j  33335  cdleme22aa  33338  cdleme22a  33339  cdleme22b  33340  cdleme22cN  33341  cdleme22d  33342  cdleme22e  33343  cdleme22eALTN  33344  cdleme22f  33345  cdleme26fALTN  33361  cdleme26f  33362  cdleme26f2ALTN  33363  cdleme26f2  33364  cdleme27N  33368  cdleme28a  33369  cdleme28b  33370  cdleme30a  33377  cdlemefs31fv1  33423  cdleme32b  33441  cdleme32c  33442  cdleme32e  33444  cdleme35h  33455  cdleme36a  33459  cdleme36m  33460  cdleme41sn3aw  33473  cdleme41sn4aw  33474  cdleme41fva11  33476  cdleme42k  33483  cdleme43cN  33490  cdleme46f2g1  33493  cdlemeg46fjgN  33520  cdlemeg46fjv  33522  cdlemeg46frv  33524  cdlemeg46rgv  33527  cdlemeg46req  33528  cdlemeg46gfv  33529  cdleme50trn2a  33549  cdlemg4a  33607  cdlemg4d  33612  cdlemg4e  33613  cdlemg4f  33614  cdlemg8c  33628  cdlemg9a  33631  cdlemg9b  33632  cdlemg10a  33639  cdlemg10  33640  cdlemg12b  33643  cdlemg12f  33647  cdlemg12g  33648  cdlemg12  33649  cdlemg17dN  33662  cdlemg17dALTN  33663  cdlemg17e  33664  cdlemg17f  33665  cdlemg17g  33666  cdlemg17i  33668  cdlemg17ir  33669  cdlemg17pq  33671  cdlemg17bq  33672  cdlemg17iqN  33673  cdlemg17  33676  cdlemg18b  33678  cdlemg18c  33679  cdlemg18d  33680  cdlemg18  33681  cdlemg19  33683  cdlemg21  33685  cdlemg28a  33692  cdlemg31b0a  33694  cdlemg27b  33695  cdlemg33b0  33700  cdlemg28b  33702  cdlemg28  33703  cdlemg35  33712  cdlemg36  33713  cdlemg44a  33730  cdlemh  33816  cdlemi2  33818  cdlemj1  33820  tendocan  33823  cdlemk5a  33834  cdlemk5  33835  cdlemki  33840  cdlemkvcl  33841  cdlemk10  33842  cdlemksv2  33846  cdlemk7  33847  cdlemk11  33848  cdlemk12  33849  cdlemkoatnle  33850  cdlemk15  33854  cdlemk16a  33855  cdlemk16  33856  cdlemk1u  33858  cdlemk5u  33860  cdlemk6u  33861  cdlemk18  33867  cdlemk19  33868  cdlemk7u  33869  cdlemk11u  33870  cdlemk12u  33871  cdlemk21N  33872  cdlemk20  33873  cdlemkoatnle-2N  33874  cdlemk13-2N  33875  cdlemkole-2N  33876  cdlemk14-2N  33877  cdlemk15-2N  33878  cdlemk16-2N  33879  cdlemk17-2N  33880  cdlemk18-2N  33885  cdlemk19-2N  33886  cdlemk22  33892  cdlemk30  33893  cdlemkuel-3  33897  cdlemkuv2-3N  33898  cdlemk18-3N  33899  cdlemkfid1N  33920  cdlemkid1  33921  cdlemkfid3N  33924  cdlemky  33925  cdlemk11ta  33928  cdlemk47  33948  cdlemk48  33949  cdlemk49  33950  cdlemk50  33951  cdlemk51  33952  cdlemk52  33953  cdlemk53a  33954  cdlemk53  33956  cdlemk54  33957  cdlemk55a  33958  cdlemkyyN  33961  cdlemk43N  33962  cdlemk55u1  33964  cdlemk55u  33965  cdlemk39u1  33966  cdlemk19u1  33968  cdleml1N  33975  cdleml2N  33976  cdleml3N  33977  dia2dimlem6  34069  cdlemn2  34195  cdlemn2a  34196  cdlemn5pre  34200  cdlemn11a  34207  dihjustlem  34216  dihjust  34217  dihmeetlem15N  34321  lclkrlem2y  34531  relexpmulnn  35668
  Copyright terms: Public domain W3C validator