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

Theorem simp22 1039
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 1006 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1027 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl22  1084  simpr22  1093  simp122  1138  simp222  1147  simp322  1156  elfiun  7942  cofsmo  8695  modexp  12400  funcoppc  15758  funcres  15779  catcisolem  15979  1stfcl  16060  2ndfcl  16061  prfcl  16066  evlfcl  16085  curf1cl  16091  curfcl  16095  hofcl  16122  mulgdirlem  16760  pmtrprfv3  17073  mdetunilem4  19617  mdetuni0  19623  mdetmul  19625  prdsxmetlem  21360  isosctrlem3  23726  isosctr  23727  amgmlem  23892  f1otrg  24878  colinearalg  24917  ax5seglem6  24941  ax5seg  24945  axpasch  24948  axeuclidlem  24969  axeuclid  24970  ogrpsub  28468  ogrpaddlt  28469  ogrpsublt  28473  rhmdvd  28573  bnj966  29744  mclspps  30211  cgrtr  30745  cgrtr3  30747  ofscom  30760  cgrextend  30761  btwnxfr  30809  colinearxfr  30828  lineext  30829  fscgr  30833  linecgr  30834  btwnconn1lem1  30840  btwnconn1lem2  30841  btwnconn1lem3  30842  btwnconn1lem4  30843  btwnconn1lem5  30844  btwnconn1lem6  30845  btwnconn1lem7  30846  seglecgr12im  30863  seglecgr12  30864  segletr  30867  broutsideof3  30879  outsideofeq  30883  lineunray  30900  linecom  30903  eqlkr  32578  lshpkrlem5  32593  omlmod1i2N  32739  cvrnbtwn3  32755  cvrcmp2  32763  cvlexch2  32808  cvlexchb2  32810  cvlatexchb2  32814  cvlatexch1  32815  cvlatexch2  32816  cvlatexch3  32817  cvlsupr7  32827  cvlsupr8  32828  atnlej1  32857  atnlej2  32858  2llnneN  32887  cvratlem  32899  atcvrneN  32908  atlelt  32916  2atjm  32923  3noncolr2  32927  3noncolr1N  32928  hlatcon2  32930  3dimlem2  32937  3dim1  32945  3dim2  32946  1cvrat  32954  ps-1  32955  ps-2  32956  2atjlej  32957  hlatexch3N  32958  ps-2b  32960  3atlem1  32961  3atlem5  32965  3atlem6  32966  2atm  33005  ps-2c  33006  lplni2  33015  lplnri3N  33033  llncvrlpln2  33035  2atmat  33039  2llnm2N  33046  2llnm3N  33047  2llnm4  33048  2llnmeqat  33049  lvolnle3at  33060  4atlem0ae  33072  4atlem0be  33073  4atlem3b  33076  4atlem9  33081  4atlem10a  33082  4atlem10  33084  4atlem11a  33085  4atlem12a  33088  4at2  33092  2lplnm2N  33099  lneq2at  33256  2llnma1b  33264  2llnma1  33265  2llnma3r  33266  2llnma2  33267  2llnma2rN  33268  cdlema1N  33269  paddasslem2  33299  paddasslem16  33313  pmodlem1  33324  pmod2iN  33327  hlmod1i  33334  atmod2i1  33339  atmod2i2  33340  atmod3i1  33342  atmod3i2  33343  atmod4i1  33344  atmod4i2  33345  llnexchb2lem  33346  llnexch2N  33348  dalawlem3  33351  dalawlem4  33352  dalawlem5  33353  dalawlem6  33354  dalawlem7  33355  dalawlem8  33356  dalawlem9  33357  dalawlem11  33359  dalawlem12  33360  dalawlem13  33361  dalawlem15  33363  osumcllem7N  33440  osumcllem9N  33442  pl42lem1N  33457  4atexlemswapqr  33541  4atex2  33555  4atex2-0bOLDN  33557  trlval4  33667  cdlemc5  33674  cdlemc6  33675  cdlemd2  33678  cdlemd4  33680  cdlemd6  33682  cdleme00a  33688  cdleme0e  33696  cdleme4  33717  cdleme4a  33718  cdleme5  33719  cdleme9  33732  cdleme16aN  33738  cdleme11c  33740  cdleme11dN  33741  cdleme11e  33742  cdleme11g  33744  cdleme11h  33745  cdleme11j  33746  cdleme11k  33747  cdleme11l  33748  cdleme11  33749  cdleme12  33750  cdleme13  33751  cdleme14  33752  cdleme15a  33753  cdleme15c  33755  cdleme16b  33758  cdleme16c  33759  cdleme16d  33760  cdleme16e  33761  cdleme16f  33762  cdleme17d1  33768  cdleme0nex  33769  cdleme18a  33770  cdleme18b  33771  cdleme18c  33772  cdleme18d  33774  cdlemednpq  33778  cdlemednuN  33779  cdleme20zN  33780  cdleme20y  33781  cdleme20yOLD  33782  cdleme19a  33783  cdleme19b  33784  cdleme19d  33786  cdleme19e  33787  cdleme20aN  33789  cdleme20d  33792  cdleme20f  33794  cdleme20g  33795  cdleme20i  33797  cdleme20j  33798  cdleme20l1  33800  cdleme20l2  33801  cdleme20l  33802  cdleme20m  33803  cdleme21b  33806  cdleme21c  33807  cdleme21e  33811  cdleme21j  33816  cdleme22aa  33819  cdleme22a  33820  cdleme22b  33821  cdleme22cN  33822  cdleme22d  33823  cdleme22e  33824  cdleme22eALTN  33825  cdleme22f  33826  cdleme26fALTN  33842  cdleme26f  33843  cdleme26f2ALTN  33844  cdleme26f2  33845  cdleme27N  33849  cdleme28a  33850  cdleme28b  33851  cdleme30a  33858  cdlemefs31fv1  33904  cdleme32b  33922  cdleme32c  33923  cdleme32e  33925  cdleme35h  33936  cdleme36a  33940  cdleme36m  33941  cdleme41sn3aw  33954  cdleme41sn4aw  33955  cdleme41fva11  33957  cdleme42k  33964  cdleme43cN  33971  cdleme46f2g1  33974  cdlemeg46fjgN  34001  cdlemeg46fjv  34003  cdlemeg46frv  34005  cdlemeg46rgv  34008  cdlemeg46req  34009  cdlemeg46gfv  34010  cdleme50trn2a  34030  cdlemg4a  34088  cdlemg4d  34093  cdlemg4e  34094  cdlemg4f  34095  cdlemg8c  34109  cdlemg9a  34112  cdlemg9b  34113  cdlemg10a  34120  cdlemg10  34121  cdlemg12b  34124  cdlemg12f  34128  cdlemg12g  34129  cdlemg12  34130  cdlemg17dN  34143  cdlemg17dALTN  34144  cdlemg17e  34145  cdlemg17f  34146  cdlemg17g  34147  cdlemg17i  34149  cdlemg17ir  34150  cdlemg17pq  34152  cdlemg17bq  34153  cdlemg17iqN  34154  cdlemg17  34157  cdlemg18b  34159  cdlemg18c  34160  cdlemg18d  34161  cdlemg18  34162  cdlemg19  34164  cdlemg21  34166  cdlemg28a  34173  cdlemg31b0a  34175  cdlemg27b  34176  cdlemg33b0  34181  cdlemg28b  34183  cdlemg28  34184  cdlemg35  34193  cdlemg36  34194  cdlemg44a  34211  cdlemh  34297  cdlemi2  34299  cdlemj1  34301  tendocan  34304  cdlemk5a  34315  cdlemk5  34316  cdlemki  34321  cdlemkvcl  34322  cdlemk10  34323  cdlemksv2  34327  cdlemk7  34328  cdlemk11  34329  cdlemk12  34330  cdlemkoatnle  34331  cdlemk15  34335  cdlemk16a  34336  cdlemk16  34337  cdlemk1u  34339  cdlemk5u  34341  cdlemk6u  34342  cdlemk18  34348  cdlemk19  34349  cdlemk7u  34350  cdlemk11u  34351  cdlemk12u  34352  cdlemk21N  34353  cdlemk20  34354  cdlemkoatnle-2N  34355  cdlemk13-2N  34356  cdlemkole-2N  34357  cdlemk14-2N  34358  cdlemk15-2N  34359  cdlemk16-2N  34360  cdlemk17-2N  34361  cdlemk18-2N  34366  cdlemk19-2N  34367  cdlemk22  34373  cdlemk30  34374  cdlemkuel-3  34378  cdlemkuv2-3N  34379  cdlemk18-3N  34380  cdlemkfid1N  34401  cdlemkid1  34402  cdlemkfid3N  34405  cdlemky  34406  cdlemk11ta  34409  cdlemk47  34429  cdlemk48  34430  cdlemk49  34431  cdlemk50  34432  cdlemk51  34433  cdlemk52  34434  cdlemk53a  34435  cdlemk53  34437  cdlemk54  34438  cdlemk55a  34439  cdlemkyyN  34442  cdlemk43N  34443  cdlemk55u1  34445  cdlemk55u  34446  cdlemk39u1  34447  cdlemk19u1  34449  cdleml1N  34456  cdleml2N  34457  cdleml3N  34458  dia2dimlem6  34550  cdlemn2  34676  cdlemn2a  34677  cdlemn5pre  34681  cdlemn11a  34688  dihjustlem  34697  dihjust  34698  dihmeetlem15N  34802  lclkrlem2y  35012  relexpmulnn  36155
  Copyright terms: Public domain W3C validator