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

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

Proof of Theorem simp23
StepHypRef Expression
1 simp3 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl23  1035  simpr23  1044  simp123  1089  simp223  1098  simp323  1107  omeulem1  6582  elfiun  7185  cofsmo  7897  modexp  11238  iscatd2  13585  funcoppc  13751  funcres  13772  catcisolem  13940  1stfcl  13973  2ndfcl  13974  prfcl  13979  evlfcl  13998  curf1cl  14004  curfcl  14008  hofcl  14035  meetle  14136  prdsxmetlem  17934  isosctrlem3  20122  isosctr  20123  colinearalg  24540  ax5seglem6  24564  ax5seg  24568  axpasch  24571  axeuclid  24593  cgrtr  24617  cgrtr3  24619  ofscom  24632  btwnxfr  24681  colinearxfr  24700  lineext  24701  brofs2  24702  brifs2  24703  fscgr  24705  linecgr  24706  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem5  24716  btwnconn1lem6  24717  btwnconn1lem7  24718  seglecgr12im  24735  seglecgr12  24736  segletr  24739  broutsideof3  24751  outsideofeq  24755  lineunray  24772  cmpmorass  25977  bisig0  26073  elhaltdp  26078  bnj966  29049  bnj967  29050  eqlkr  29362  omlmod1i2N  29523  cvrcmp2  29547  cvlexch2  29592  cvlexchb2  29594  cvlatexchb2  29598  cvlatexch1  29599  cvlatexch2  29600  cvlatexch3  29601  cvlsupr7  29611  cvlsupr8  29612  atnlej1  29641  atnlej2  29642  2llnneN  29671  cvratlem  29683  atcvrneN  29692  atcvrj1  29693  atlelt  29700  2atjm  29707  3noncolr2  29711  3noncolr1N  29712  hlatcon2  29714  3dimlem2  29721  3dim1  29729  3dim2  29730  1cvrat  29738  ps-1  29739  ps-2  29740  2atjlej  29741  hlatexch3N  29742  ps-2b  29744  3atlem1  29745  3atlem2  29746  3atlem6  29750  llnle  29780  2atm  29789  ps-2c  29790  lplni2  29799  lplnle  29802  lplnnle2at  29803  lplnri3N  29817  llncvrlpln2  29819  2atmat  29823  2llnjaN  29828  2llnm2N  29830  2llnm4  29832  2llnmeqat  29833  lvolnle3at  29844  4atlem0ae  29856  4atlem0be  29857  4atlem3b  29860  4atlem9  29865  4atlem10a  29866  4atlem10  29868  4atlem11a  29869  4atlem12a  29872  4at  29875  4at2  29876  lplncvrlvol2  29877  2lplnm2N  29883  2llnma1b  30048  2llnma1  30049  2llnma3r  30050  2llnma2  30051  2llnma2rN  30052  cdlema1N  30053  cdlema2N  30054  paddasslem2  30083  paddasslem15  30096  paddasslem16  30097  pmodlem1  30108  pmod2iN  30111  hlmod1i  30118  atmod2i1  30123  atmod2i2  30124  atmod3i1  30126  atmod3i2  30127  atmod4i1  30128  atmod4i2  30129  llnexchb2  30131  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem9  30141  dalawlem11  30143  dalawlem13  30145  dalawlem15  30147  osumcllem7N  30224  osumcllem9N  30226  osumcllem11N  30228  pl42lem1N  30241  4atex  30338  4atex2-0aOLDN  30340  4atex2-0bOLDN  30341  4atex2-0cOLDN  30342  trlval4  30450  cdlemc5  30457  cdlemd5  30464  cdlemd6  30465  cdleme00a  30471  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4  30500  cdleme4a  30501  cdleme16aN  30521  cdleme11c  30523  cdleme11g  30527  cdleme11h  30528  cdleme12  30533  cdleme0nex  30552  cdleme18a  30553  cdleme18b  30554  cdleme18c  30555  cdleme18d  30557  cdleme20zN  30563  cdleme20y  30564  cdleme19a  30565  cdleme19b  30566  cdleme19d  30568  cdleme19e  30569  cdleme20aN  30571  cdleme20c  30573  cdleme20d  30574  cdleme20i  30579  cdleme20j  30580  cdleme20l1  30582  cdleme20l2  30583  cdleme20m  30585  cdleme21b  30588  cdleme21c  30589  cdleme21j  30598  cdleme22aa  30601  cdleme22a  30602  cdleme22eALTN  30607  cdleme26e  30621  cdleme26fALTN  30624  cdleme26f  30625  cdleme26f2ALTN  30626  cdleme26f2  30627  cdleme27N  30631  cdleme28a  30632  cdleme28b  30633  cdleme30a  30640  cdlemefs45eN  30693  cdleme32c  30705  cdleme32e  30707  cdleme35h  30718  cdleme36a  30722  cdleme36m  30723  cdleme37m  30724  cdleme41sn3aw  30736  cdleme41sn4aw  30737  cdleme41fva11  30739  cdleme42k  30746  cdleme43cN  30753  cdleme43dN  30754  cdleme46f2g1  30756  cdlemeg47rv2  30772  cdlemeg46sfg  30782  cdlemeg46fjgN  30783  cdlemeg46rjgN  30784  cdlemeg46fjv  30785  cdlemeg46frv  30787  cdlemeg46vrg  30789  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfv  30792  cdleme50trn2a  30812  cdlemg2fv2  30862  cdlemg4a  30870  cdlemg4e  30876  cdlemg4f  30877  cdlemg8b  30890  cdlemg8c  30891  cdlemg9a  30894  cdlemg9b  30895  cdlemg9  30896  cdlemg10a  30902  cdlemg12a  30905  cdlemg12b  30906  cdlemg12c  30907  cdlemg12  30912  cdlemg17dN  30925  cdlemg17dALTN  30926  cdlemg17e  30927  cdlemg17i  30931  cdlemg17ir  30932  cdlemg17pq  30934  cdlemg17bq  30935  cdlemg17iqN  30936  cdlemg17  30939  cdlemg18b  30941  cdlemg18c  30942  cdlemg18d  30943  cdlemg18  30944  cdlemg19  30946  cdlemg21  30948  cdlemg28a  30955  cdlemg31b0a  30957  cdlemg33b0  30963  cdlemg35  30975  cdlemg44a  30993  cdlemh  31079  cdlemi2  31081  cdlemj1  31083  cdlemk5a  31097  cdlemk5  31098  cdlemki  31103  cdlemkvcl  31104  cdlemk10  31105  cdlemksv2  31109  cdlemk7  31110  cdlemk11  31111  cdlemk12  31112  cdlemk15  31117  cdlemk16a  31118  cdlemk16  31119  cdlemk5u  31123  cdlemk6u  31124  cdlemk18  31130  cdlemk19  31131  cdlemk7u  31132  cdlemk11u  31133  cdlemk12u  31134  cdlemk21N  31135  cdlemk20  31136  cdlemkoatnle-2N  31137  cdlemk13-2N  31138  cdlemkole-2N  31139  cdlemk14-2N  31140  cdlemk15-2N  31141  cdlemk16-2N  31142  cdlemk17-2N  31143  cdlemk18-2N  31148  cdlemk19-2N  31149  cdlemk22  31155  cdlemk30  31156  cdlemk28-3  31170  cdlemk33N  31171  cdlemkfid1N  31183  cdlemkid1  31184  cdlemky  31188  cdlemk11ta  31191  cdlemk35s-id  31200  cdlemk39s-id  31202  cdlemk47  31211  cdlemk48  31212  cdlemk49  31213  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk53a  31217  cdlemk53b  31218  cdlemk53  31219  cdlemk54  31220  cdlemk55a  31221  cdlemkyyN  31224  cdlemk43N  31225  cdlemk55u1  31227  cdlemk55u  31228  cdlemk39u1  31229  cdlemk19u1  31231  cdleml1N  31238  cdleml2N  31239  cdleml3N  31240  dia2dimlem6  31332  cdlemn2  31458  cdlemn2a  31459  cdlemn5pre  31463  cdlemn11pre  31473  dihjustlem  31479  dihjust  31480  dihmeetlem15N  31584  lclkrlem2y  31794
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