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  7273  cofsmo  7985  modexp  11329  funcoppc  13848  funcres  13869  catcisolem  14037  1stfcl  14070  2ndfcl  14071  prfcl  14076  evlfcl  14095  curf1cl  14101  curfcl  14105  hofcl  14132  meetle  14233  mulgdirlem  14690  prdsxmetlem  18034  isosctrlem3  20231  isosctr  20232  amgmlem  20395  rhmdvd  23425  colinearalg  25097  ax5seglem6  25121  ax5seg  25125  axpasch  25128  axeuclidlem  25149  axeuclid  25150  cgrtr  25174  cgrtr3  25176  ofscom  25189  cgrextend  25190  btwnxfr  25238  colinearxfr  25257  lineext  25258  fscgr  25262  linecgr  25263  btwnconn1lem1  25269  btwnconn1lem2  25270  btwnconn1lem3  25271  btwnconn1lem4  25272  btwnconn1lem5  25273  btwnconn1lem6  25274  btwnconn1lem7  25275  seglecgr12im  25292  seglecgr12  25293  segletr  25296  broutsideof3  25308  outsideofeq  25312  lineunray  25329  linecom  25332  bnj966  28738  eqlkr  29358  lshpkrlem5  29373  omlmod1i2N  29519  cvrnbtwn3  29535  cvrcmp2  29543  cvlexch2  29588  cvlexchb2  29590  cvlatexchb2  29594  cvlatexch1  29595  cvlatexch2  29596  cvlatexch3  29597  cvlsupr7  29607  cvlsupr8  29608  atnlej1  29637  atnlej2  29638  2llnneN  29667  cvratlem  29679  atcvrneN  29688  atlelt  29696  2atjm  29703  3noncolr2  29707  3noncolr1N  29708  hlatcon2  29710  3dimlem2  29717  3dim1  29725  3dim2  29726  1cvrat  29734  ps-1  29735  ps-2  29736  2atjlej  29737  hlatexch3N  29738  ps-2b  29740  3atlem1  29741  3atlem5  29745  3atlem6  29746  2atm  29785  ps-2c  29786  lplni2  29795  lplnri3N  29813  llncvrlpln2  29815  2atmat  29819  2llnm2N  29826  2llnm3N  29827  2llnm4  29828  2llnmeqat  29829  lvolnle3at  29840  4atlem0ae  29852  4atlem0be  29853  4atlem3b  29856  4atlem9  29861  4atlem10a  29862  4atlem10  29864  4atlem11a  29865  4atlem12a  29868  4at2  29872  2lplnm2N  29879  lneq2at  30036  2llnma1b  30044  2llnma1  30045  2llnma3r  30046  2llnma2  30047  2llnma2rN  30048  cdlema1N  30049  paddasslem2  30079  paddasslem16  30093  pmodlem1  30104  pmod2iN  30107  hlmod1i  30114  atmod2i1  30119  atmod2i2  30120  atmod3i1  30122  atmod3i2  30123  atmod4i1  30124  atmod4i2  30125  llnexchb2lem  30126  llnexch2N  30128  dalawlem3  30131  dalawlem4  30132  dalawlem5  30133  dalawlem6  30134  dalawlem7  30135  dalawlem8  30136  dalawlem9  30137  dalawlem11  30139  dalawlem12  30140  dalawlem13  30141  dalawlem15  30143  osumcllem7N  30220  osumcllem9N  30222  pl42lem1N  30237  4atexlemswapqr  30321  4atex2  30335  4atex2-0bOLDN  30337  trlval4  30446  cdlemc5  30453  cdlemc6  30454  cdlemd2  30457  cdlemd4  30459  cdlemd6  30461  cdleme00a  30467  cdleme0e  30475  cdleme4  30496  cdleme4a  30497  cdleme5  30498  cdleme9  30511  cdleme16aN  30517  cdleme11c  30519  cdleme11dN  30520  cdleme11e  30521  cdleme11g  30523  cdleme11h  30524  cdleme11j  30525  cdleme11k  30526  cdleme11l  30527  cdleme11  30528  cdleme12  30529  cdleme13  30530  cdleme14  30531  cdleme15a  30532  cdleme15c  30534  cdleme16b  30537  cdleme16c  30538  cdleme16d  30539  cdleme16e  30540  cdleme16f  30541  cdleme17d1  30547  cdleme0nex  30548  cdleme18a  30549  cdleme18b  30550  cdleme18c  30551  cdleme18d  30553  cdlemednpq  30557  cdlemednuN  30558  cdleme20zN  30559  cdleme20y  30560  cdleme19a  30561  cdleme19b  30562  cdleme19d  30564  cdleme19e  30565  cdleme20aN  30567  cdleme20d  30570  cdleme20f  30572  cdleme20g  30573  cdleme20i  30575  cdleme20j  30576  cdleme20l1  30578  cdleme20l2  30579  cdleme20l  30580  cdleme20m  30581  cdleme21b  30584  cdleme21c  30585  cdleme21e  30589  cdleme21j  30594  cdleme22aa  30597  cdleme22a  30598  cdleme22b  30599  cdleme22cN  30600  cdleme22d  30601  cdleme22e  30602  cdleme22eALTN  30603  cdleme22f  30604  cdleme26fALTN  30620  cdleme26f  30621  cdleme26f2ALTN  30622  cdleme26f2  30623  cdleme27N  30627  cdleme28a  30628  cdleme28b  30629  cdleme30a  30636  cdlemefs31fv1  30682  cdleme32b  30700  cdleme32c  30701  cdleme32e  30703  cdleme35h  30714  cdleme36a  30718  cdleme36m  30719  cdleme41sn3aw  30732  cdleme41sn4aw  30733  cdleme41fva11  30735  cdleme42k  30742  cdleme43cN  30749  cdleme46f2g1  30752  cdlemeg46fjgN  30779  cdlemeg46fjv  30781  cdlemeg46frv  30783  cdlemeg46rgv  30786  cdlemeg46req  30787  cdlemeg46gfv  30788  cdleme50trn2a  30808  cdlemg4a  30866  cdlemg4d  30871  cdlemg4e  30872  cdlemg4f  30873  cdlemg8c  30887  cdlemg9a  30890  cdlemg9b  30891  cdlemg10a  30898  cdlemg10  30899  cdlemg12b  30902  cdlemg12f  30906  cdlemg12g  30907  cdlemg12  30908  cdlemg17dN  30921  cdlemg17dALTN  30922  cdlemg17e  30923  cdlemg17f  30924  cdlemg17g  30925  cdlemg17i  30927  cdlemg17ir  30928  cdlemg17pq  30930  cdlemg17bq  30931  cdlemg17iqN  30932  cdlemg17  30935  cdlemg18b  30937  cdlemg18c  30938  cdlemg18d  30939  cdlemg18  30940  cdlemg19  30942  cdlemg21  30944  cdlemg28a  30951  cdlemg31b0a  30953  cdlemg27b  30954  cdlemg33b0  30959  cdlemg28b  30961  cdlemg28  30962  cdlemg35  30971  cdlemg36  30972  cdlemg44a  30989  cdlemh  31075  cdlemi2  31077  cdlemj1  31079  tendocan  31082  cdlemk5a  31093  cdlemk5  31094  cdlemki  31099  cdlemkvcl  31100  cdlemk10  31101  cdlemksv2  31105  cdlemk7  31106  cdlemk11  31107  cdlemk12  31108  cdlemkoatnle  31109  cdlemk15  31113  cdlemk16a  31114  cdlemk16  31115  cdlemk1u  31117  cdlemk5u  31119  cdlemk6u  31120  cdlemk18  31126  cdlemk19  31127  cdlemk7u  31128  cdlemk11u  31129  cdlemk12u  31130  cdlemk21N  31131  cdlemk20  31132  cdlemkoatnle-2N  31133  cdlemk13-2N  31134  cdlemkole-2N  31135  cdlemk14-2N  31136  cdlemk15-2N  31137  cdlemk16-2N  31138  cdlemk17-2N  31139  cdlemk18-2N  31144  cdlemk19-2N  31145  cdlemk22  31151  cdlemk30  31152  cdlemkuel-3  31156  cdlemkuv2-3N  31157  cdlemk18-3N  31158  cdlemkfid1N  31179  cdlemkid1  31180  cdlemkfid3N  31183  cdlemky  31184  cdlemk11ta  31187  cdlemk47  31207  cdlemk48  31208  cdlemk49  31209  cdlemk50  31210  cdlemk51  31211  cdlemk52  31212  cdlemk53a  31213  cdlemk53  31215  cdlemk54  31216  cdlemk55a  31217  cdlemkyyN  31220  cdlemk43N  31221  cdlemk55u1  31223  cdlemk55u  31224  cdlemk39u1  31225  cdlemk19u1  31227  cdleml1N  31234  cdleml2N  31235  cdleml3N  31236  dia2dimlem6  31328  cdlemn2  31454  cdlemn2a  31455  cdlemn5pre  31459  cdlemn11a  31466  dihjustlem  31475  dihjust  31476  dihmeetlem15N  31580  lclkrlem2y  31790
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