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

Theorem simp22 989
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 956 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl22  1034  simpr22  1043  simp122  1088  simp222  1097  simp322  1106  elfiun  7183  cofsmo  7895  modexp  11236  funcoppc  13749  funcres  13770  catcisolem  13938  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  meetle  14134  mulgdirlem  14591  prdsxmetlem  17932  isosctrlem3  20120  isosctr  20121  amgmlem  20284  colinearalg  24538  ax5seglem6  24562  ax5seg  24566  axpasch  24569  axeuclidlem  24590  axeuclid  24591  cgrtr  24615  cgrtr3  24617  ofscom  24630  cgrextend  24631  btwnxfr  24679  colinearxfr  24698  lineext  24699  fscgr  24703  linecgr  24704  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  seglecgr12im  24733  seglecgr12  24734  segletr  24737  broutsideof3  24749  outsideofeq  24753  lineunray  24770  linecom  24773  cmpmorass  25966  bisig0  26062  isig22  26065  bnj966  28976  eqlkr  29289  lshpkrlem5  29304  omlmod1i2N  29450  cvrnbtwn3  29466  cvrcmp2  29474  cvlexch2  29519  cvlexchb2  29521  cvlatexchb2  29525  cvlatexch1  29526  cvlatexch2  29527  cvlatexch3  29528  cvlsupr7  29538  cvlsupr8  29539  atnlej1  29568  atnlej2  29569  2llnneN  29598  cvratlem  29610  atcvrneN  29619  atlelt  29627  2atjm  29634  3noncolr2  29638  3noncolr1N  29639  hlatcon2  29641  3dimlem2  29648  3dim1  29656  3dim2  29657  1cvrat  29665  ps-1  29666  ps-2  29667  2atjlej  29668  hlatexch3N  29669  ps-2b  29671  3atlem1  29672  3atlem5  29676  3atlem6  29677  2atm  29716  ps-2c  29717  lplni2  29726  lplnri3N  29744  llncvrlpln2  29746  2atmat  29750  2llnm2N  29757  2llnm3N  29758  2llnm4  29759  2llnmeqat  29760  lvolnle3at  29771  4atlem0ae  29783  4atlem0be  29784  4atlem3b  29787  4atlem9  29792  4atlem10a  29793  4atlem10  29795  4atlem11a  29796  4atlem12a  29799  4at2  29803  2lplnm2N  29810  lneq2at  29967  2llnma1b  29975  2llnma1  29976  2llnma3r  29977  2llnma2  29978  2llnma2rN  29979  cdlema1N  29980  paddasslem2  30010  paddasslem16  30024  pmodlem1  30035  pmod2iN  30038  hlmod1i  30045  atmod2i1  30050  atmod2i2  30051  atmod3i1  30053  atmod3i2  30054  atmod4i1  30055  atmod4i2  30056  llnexchb2lem  30057  llnexch2N  30059  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  dalawlem13  30072  dalawlem15  30074  osumcllem7N  30151  osumcllem9N  30153  pl42lem1N  30168  4atexlemswapqr  30252  4atex2  30266  4atex2-0bOLDN  30268  trlval4  30377  cdlemc5  30384  cdlemc6  30385  cdlemd2  30388  cdlemd4  30390  cdlemd6  30392  cdleme00a  30398  cdleme0e  30406  cdleme4  30427  cdleme4a  30428  cdleme5  30429  cdleme9  30442  cdleme16aN  30448  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11g  30454  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme11l  30458  cdleme11  30459  cdleme12  30460  cdleme13  30461  cdleme14  30462  cdleme15a  30463  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17d1  30478  cdleme0nex  30479  cdleme18a  30480  cdleme18b  30481  cdleme18c  30482  cdleme18d  30484  cdlemednpq  30488  cdlemednuN  30489  cdleme20zN  30490  cdleme20y  30491  cdleme19a  30492  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20aN  30498  cdleme20d  30501  cdleme20f  30503  cdleme20g  30504  cdleme20i  30506  cdleme20j  30507  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21b  30515  cdleme21c  30516  cdleme21e  30520  cdleme21j  30525  cdleme22aa  30528  cdleme22a  30529  cdleme22b  30530  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme30a  30567  cdlemefs31fv1  30613  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35h  30645  cdleme36a  30649  cdleme36m  30650  cdleme41sn3aw  30663  cdleme41sn4aw  30664  cdleme41fva11  30666  cdleme42k  30673  cdleme43cN  30680  cdleme46f2g1  30683  cdlemeg46fjgN  30710  cdlemeg46fjv  30712  cdlemeg46frv  30714  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdleme50trn2a  30739  cdlemg4a  30797  cdlemg4d  30802  cdlemg4e  30803  cdlemg4f  30804  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg10a  30829  cdlemg10  30830  cdlemg12b  30833  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg17dN  30852  cdlemg17dALTN  30853  cdlemg17e  30854  cdlemg17f  30855  cdlemg17g  30856  cdlemg17i  30858  cdlemg17ir  30859  cdlemg17pq  30861  cdlemg17bq  30862  cdlemg17iqN  30863  cdlemg17  30866  cdlemg18b  30868  cdlemg18c  30869  cdlemg18d  30870  cdlemg18  30871  cdlemg19  30873  cdlemg21  30875  cdlemg28a  30882  cdlemg31b0a  30884  cdlemg27b  30885  cdlemg33b0  30890  cdlemg28b  30892  cdlemg28  30893  cdlemg35  30902  cdlemg36  30903  cdlemg44a  30920  cdlemh  31006  cdlemi2  31008  cdlemj1  31010  tendocan  31013  cdlemk5a  31024  cdlemk5  31025  cdlemki  31030  cdlemkvcl  31031  cdlemk10  31032  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkoatnle  31040  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  cdlemk1u  31048  cdlemk5u  31050  cdlemk6u  31051  cdlemk18  31057  cdlemk19  31058  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk22  31082  cdlemk30  31083  cdlemkuel-3  31087  cdlemkuv2-3N  31088  cdlemk18-3N  31089  cdlemkfid1N  31110  cdlemkid1  31111  cdlemkfid3N  31114  cdlemky  31115  cdlemk11ta  31118  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk53  31146  cdlemk54  31147  cdlemk55a  31148  cdlemkyyN  31151  cdlemk43N  31152  cdlemk55u1  31154  cdlemk55u  31155  cdlemk39u1  31156  cdlemk19u1  31158  cdleml1N  31165  cdleml2N  31166  cdleml3N  31167  dia2dimlem6  31259  cdlemn2  31385  cdlemn2a  31386  cdlemn5pre  31390  cdlemn11a  31397  dihjustlem  31406  dihjust  31407  dihmeetlem15N  31511  lclkrlem2y  31721
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