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  6580  elfiun  7183  cofsmo  7895  modexp  11236  iscatd2  13583  funcoppc  13749  funcres  13770  catcisolem  13938  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  meetle  14134  prdsxmetlem  17932  isosctrlem3  20120  isosctr  20121  colinearalg  24538  ax5seglem6  24562  ax5seg  24566  axpasch  24569  axeuclid  24591  cgrtr  24615  cgrtr3  24617  ofscom  24630  btwnxfr  24679  colinearxfr  24698  lineext  24699  brofs2  24700  brifs2  24701  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  cmpmorass  25966  bisig0  26062  elhaltdp  26067  bnj966  28976  bnj967  28977  eqlkr  29289  omlmod1i2N  29450  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  atcvrj1  29620  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  3atlem2  29673  3atlem6  29677  llnle  29707  2atm  29716  ps-2c  29717  lplni2  29726  lplnle  29729  lplnnle2at  29730  lplnri3N  29744  llncvrlpln2  29746  2atmat  29750  2llnjaN  29755  2llnm2N  29757  2llnm4  29759  2llnmeqat  29760  lvolnle3at  29771  4atlem0ae  29783  4atlem0be  29784  4atlem3b  29787  4atlem9  29792  4atlem10a  29793  4atlem10  29795  4atlem11a  29796  4atlem12a  29799  4at  29802  4at2  29803  lplncvrlvol2  29804  2lplnm2N  29810  2llnma1b  29975  2llnma1  29976  2llnma3r  29977  2llnma2  29978  2llnma2rN  29979  cdlema1N  29980  cdlema2N  29981  paddasslem2  30010  paddasslem15  30023  paddasslem16  30024  pmodlem1  30035  pmod2iN  30038  hlmod1i  30045  atmod2i1  30050  atmod2i2  30051  atmod3i1  30053  atmod3i2  30054  atmod4i1  30055  atmod4i2  30056  llnexchb2  30058  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem11  30070  dalawlem13  30072  dalawlem15  30074  osumcllem7N  30151  osumcllem9N  30153  osumcllem11N  30155  pl42lem1N  30168  4atex  30265  4atex2-0aOLDN  30267  4atex2-0bOLDN  30268  4atex2-0cOLDN  30269  trlval4  30377  cdlemc5  30384  cdlemd5  30391  cdlemd6  30392  cdleme00a  30398  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme4  30427  cdleme4a  30428  cdleme16aN  30448  cdleme11c  30450  cdleme11g  30454  cdleme11h  30455  cdleme12  30460  cdleme0nex  30479  cdleme18a  30480  cdleme18b  30481  cdleme18c  30482  cdleme18d  30484  cdleme20zN  30490  cdleme20y  30491  cdleme19a  30492  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20aN  30498  cdleme20c  30500  cdleme20d  30501  cdleme20i  30506  cdleme20j  30507  cdleme20l1  30509  cdleme20l2  30510  cdleme20m  30512  cdleme21b  30515  cdleme21c  30516  cdleme21j  30525  cdleme22aa  30528  cdleme22a  30529  cdleme22eALTN  30534  cdleme26e  30548  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme30a  30567  cdlemefs45eN  30620  cdleme32c  30632  cdleme32e  30634  cdleme35h  30645  cdleme36a  30649  cdleme36m  30650  cdleme37m  30651  cdleme41sn3aw  30663  cdleme41sn4aw  30664  cdleme41fva11  30666  cdleme42k  30673  cdleme43cN  30680  cdleme43dN  30681  cdleme46f2g1  30683  cdlemeg47rv2  30699  cdlemeg46sfg  30709  cdlemeg46fjgN  30710  cdlemeg46rjgN  30711  cdlemeg46fjv  30712  cdlemeg46frv  30714  cdlemeg46vrg  30716  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdleme50trn2a  30739  cdlemg2fv2  30789  cdlemg4a  30797  cdlemg4e  30803  cdlemg4f  30804  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg9  30823  cdlemg10a  30829  cdlemg12a  30832  cdlemg12b  30833  cdlemg12c  30834  cdlemg12  30839  cdlemg17dN  30852  cdlemg17dALTN  30853  cdlemg17e  30854  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  cdlemg33b0  30890  cdlemg35  30902  cdlemg44a  30920  cdlemh  31006  cdlemi2  31008  cdlemj1  31010  cdlemk5a  31024  cdlemk5  31025  cdlemki  31030  cdlemkvcl  31031  cdlemk10  31032  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  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  cdlemk28-3  31097  cdlemk33N  31098  cdlemkfid1N  31110  cdlemkid1  31111  cdlemky  31115  cdlemk11ta  31118  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk53b  31145  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  cdlemn11pre  31400  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