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

Theorem simp22 991
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl22  1036  simpr22  1045  simp122  1090  simp222  1099  simp322  1108  elfiun  7421  cofsmo  8133  modexp  11497  funcoppc  14055  funcres  14076  catcisolem  14244  1stfcl  14277  2ndfcl  14278  prfcl  14283  evlfcl  14302  curf1cl  14308  curfcl  14312  hofcl  14339  meetle  14440  mulgdirlem  14897  prdsxmetlem  18381  isosctrlem3  20647  isosctr  20648  amgmlem  20811  ofldaddlt  24224  rhmdvd  24242  colinearalg  25792  ax5seglem6  25816  ax5seg  25820  axpasch  25823  axeuclidlem  25844  axeuclid  25845  cgrtr  25869  cgrtr3  25871  ofscom  25884  cgrextend  25885  btwnxfr  25933  colinearxfr  25952  lineext  25953  fscgr  25957  linecgr  25958  btwnconn1lem1  25964  btwnconn1lem2  25965  btwnconn1lem3  25966  btwnconn1lem4  25967  btwnconn1lem5  25968  btwnconn1lem6  25969  btwnconn1lem7  25970  seglecgr12im  25987  seglecgr12  25988  segletr  25991  broutsideof3  26003  outsideofeq  26007  lineunray  26024  linecom  26027  bnj966  29067  eqlkr  29628  lshpkrlem5  29643  omlmod1i2N  29789  cvrnbtwn3  29805  cvrcmp2  29813  cvlexch2  29858  cvlexchb2  29860  cvlatexchb2  29864  cvlatexch1  29865  cvlatexch2  29866  cvlatexch3  29867  cvlsupr7  29877  cvlsupr8  29878  atnlej1  29907  atnlej2  29908  2llnneN  29937  cvratlem  29949  atcvrneN  29958  atlelt  29966  2atjm  29973  3noncolr2  29977  3noncolr1N  29978  hlatcon2  29980  3dimlem2  29987  3dim1  29995  3dim2  29996  1cvrat  30004  ps-1  30005  ps-2  30006  2atjlej  30007  hlatexch3N  30008  ps-2b  30010  3atlem1  30011  3atlem5  30015  3atlem6  30016  2atm  30055  ps-2c  30056  lplni2  30065  lplnri3N  30083  llncvrlpln2  30085  2atmat  30089  2llnm2N  30096  2llnm3N  30097  2llnm4  30098  2llnmeqat  30099  lvolnle3at  30110  4atlem0ae  30122  4atlem0be  30123  4atlem3b  30126  4atlem9  30131  4atlem10a  30132  4atlem10  30134  4atlem11a  30135  4atlem12a  30138  4at2  30142  2lplnm2N  30149  lneq2at  30306  2llnma1b  30314  2llnma1  30315  2llnma3r  30316  2llnma2  30317  2llnma2rN  30318  cdlema1N  30319  paddasslem2  30349  paddasslem16  30363  pmodlem1  30374  pmod2iN  30377  hlmod1i  30384  atmod2i1  30389  atmod2i2  30390  atmod3i1  30392  atmod3i2  30393  atmod4i1  30394  atmod4i2  30395  llnexchb2lem  30396  llnexch2N  30398  dalawlem3  30401  dalawlem4  30402  dalawlem5  30403  dalawlem6  30404  dalawlem7  30405  dalawlem8  30406  dalawlem9  30407  dalawlem11  30409  dalawlem12  30410  dalawlem13  30411  dalawlem15  30413  osumcllem7N  30490  osumcllem9N  30492  pl42lem1N  30507  4atexlemswapqr  30591  4atex2  30605  4atex2-0bOLDN  30607  trlval4  30716  cdlemc5  30723  cdlemc6  30724  cdlemd2  30727  cdlemd4  30729  cdlemd6  30731  cdleme00a  30737  cdleme0e  30745  cdleme4  30766  cdleme4a  30767  cdleme5  30768  cdleme9  30781  cdleme16aN  30787  cdleme11c  30789  cdleme11dN  30790  cdleme11e  30791  cdleme11g  30793  cdleme11h  30794  cdleme11j  30795  cdleme11k  30796  cdleme11l  30797  cdleme11  30798  cdleme12  30799  cdleme13  30800  cdleme14  30801  cdleme15a  30802  cdleme15c  30804  cdleme16b  30807  cdleme16c  30808  cdleme16d  30809  cdleme16e  30810  cdleme16f  30811  cdleme17d1  30817  cdleme0nex  30818  cdleme18a  30819  cdleme18b  30820  cdleme18c  30821  cdleme18d  30823  cdlemednpq  30827  cdlemednuN  30828  cdleme20zN  30829  cdleme20y  30830  cdleme19a  30831  cdleme19b  30832  cdleme19d  30834  cdleme19e  30835  cdleme20aN  30837  cdleme20d  30840  cdleme20f  30842  cdleme20g  30843  cdleme20i  30845  cdleme20j  30846  cdleme20l1  30848  cdleme20l2  30849  cdleme20l  30850  cdleme20m  30851  cdleme21b  30854  cdleme21c  30855  cdleme21e  30859  cdleme21j  30864  cdleme22aa  30867  cdleme22a  30868  cdleme22b  30869  cdleme22cN  30870  cdleme22d  30871  cdleme22e  30872  cdleme22eALTN  30873  cdleme22f  30874  cdleme26fALTN  30890  cdleme26f  30891  cdleme26f2ALTN  30892  cdleme26f2  30893  cdleme27N  30897  cdleme28a  30898  cdleme28b  30899  cdleme30a  30906  cdlemefs31fv1  30952  cdleme32b  30970  cdleme32c  30971  cdleme32e  30973  cdleme35h  30984  cdleme36a  30988  cdleme36m  30989  cdleme41sn3aw  31002  cdleme41sn4aw  31003  cdleme41fva11  31005  cdleme42k  31012  cdleme43cN  31019  cdleme46f2g1  31022  cdlemeg46fjgN  31049  cdlemeg46fjv  31051  cdlemeg46frv  31053  cdlemeg46rgv  31056  cdlemeg46req  31057  cdlemeg46gfv  31058  cdleme50trn2a  31078  cdlemg4a  31136  cdlemg4d  31141  cdlemg4e  31142  cdlemg4f  31143  cdlemg8c  31157  cdlemg9a  31160  cdlemg9b  31161  cdlemg10a  31168  cdlemg10  31169  cdlemg12b  31172  cdlemg12f  31176  cdlemg12g  31177  cdlemg12  31178  cdlemg17dN  31191  cdlemg17dALTN  31192  cdlemg17e  31193  cdlemg17f  31194  cdlemg17g  31195  cdlemg17i  31197  cdlemg17ir  31198  cdlemg17pq  31200  cdlemg17bq  31201  cdlemg17iqN  31202  cdlemg17  31205  cdlemg18b  31207  cdlemg18c  31208  cdlemg18d  31209  cdlemg18  31210  cdlemg19  31212  cdlemg21  31214  cdlemg28a  31221  cdlemg31b0a  31223  cdlemg27b  31224  cdlemg33b0  31229  cdlemg28b  31231  cdlemg28  31232  cdlemg35  31241  cdlemg36  31242  cdlemg44a  31259  cdlemh  31345  cdlemi2  31347  cdlemj1  31349  tendocan  31352  cdlemk5a  31363  cdlemk5  31364  cdlemki  31369  cdlemkvcl  31370  cdlemk10  31371  cdlemksv2  31375  cdlemk7  31376  cdlemk11  31377  cdlemk12  31378  cdlemkoatnle  31379  cdlemk15  31383  cdlemk16a  31384  cdlemk16  31385  cdlemk1u  31387  cdlemk5u  31389  cdlemk6u  31390  cdlemk18  31396  cdlemk19  31397  cdlemk7u  31398  cdlemk11u  31399  cdlemk12u  31400  cdlemk21N  31401  cdlemk20  31402  cdlemkoatnle-2N  31403  cdlemk13-2N  31404  cdlemkole-2N  31405  cdlemk14-2N  31406  cdlemk15-2N  31407  cdlemk16-2N  31408  cdlemk17-2N  31409  cdlemk18-2N  31414  cdlemk19-2N  31415  cdlemk22  31421  cdlemk30  31422  cdlemkuel-3  31426  cdlemkuv2-3N  31427  cdlemk18-3N  31428  cdlemkfid1N  31449  cdlemkid1  31450  cdlemkfid3N  31453  cdlemky  31454  cdlemk11ta  31457  cdlemk47  31477  cdlemk48  31478  cdlemk49  31479  cdlemk50  31480  cdlemk51  31481  cdlemk52  31482  cdlemk53a  31483  cdlemk53  31485  cdlemk54  31486  cdlemk55a  31487  cdlemkyyN  31490  cdlemk43N  31491  cdlemk55u1  31493  cdlemk55u  31494  cdlemk39u1  31495  cdlemk19u1  31497  cdleml1N  31504  cdleml2N  31505  cdleml3N  31506  dia2dimlem6  31598  cdlemn2  31724  cdlemn2a  31725  cdlemn5pre  31729  cdlemn11a  31736  dihjustlem  31745  dihjust  31746  dihmeetlem15N  31850  lclkrlem2y  32060
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