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

Theorem simp23 992
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl23  1037  simpr23  1046  simp123  1091  simp223  1100  simp323  1109  funtpg  5492  omeulem1  6816  elfiun  7426  cofsmo  8138  modexp  11502  iscatd2  13894  funcoppc  14060  funcres  14081  catcisolem  14249  1stfcl  14282  2ndfcl  14283  prfcl  14288  evlfcl  14307  curf1cl  14313  curfcl  14317  hofcl  14344  meetle  14445  prdsxmetlem  18386  isosctrlem3  20652  isosctr  20653  rhmdvd  24247  colinearalg  25797  ax5seglem6  25821  ax5seg  25825  axpasch  25828  axeuclid  25850  cgrtr  25874  cgrtr3  25876  ofscom  25889  btwnxfr  25938  colinearxfr  25957  lineext  25958  brofs2  25959  brifs2  25960  fscgr  25962  linecgr  25963  btwnconn1lem1  25969  btwnconn1lem2  25970  btwnconn1lem3  25971  btwnconn1lem4  25972  btwnconn1lem5  25973  btwnconn1lem6  25974  btwnconn1lem7  25975  seglecgr12im  25992  seglecgr12  25993  segletr  25996  broutsideof3  26008  outsideofeq  26012  lineunray  26029  bnj966  29169  bnj967  29170  eqlkr  29736  omlmod1i2N  29897  cvrcmp2  29921  cvlexch2  29966  cvlexchb2  29968  cvlatexchb2  29972  cvlatexch1  29973  cvlatexch2  29974  cvlatexch3  29975  cvlsupr7  29985  cvlsupr8  29986  atnlej1  30015  atnlej2  30016  2llnneN  30045  cvratlem  30057  atcvrneN  30066  atcvrj1  30067  atlelt  30074  2atjm  30081  3noncolr2  30085  3noncolr1N  30086  hlatcon2  30088  3dimlem2  30095  3dim1  30103  3dim2  30104  1cvrat  30112  ps-1  30113  ps-2  30114  2atjlej  30115  hlatexch3N  30116  ps-2b  30118  3atlem1  30119  3atlem2  30120  3atlem6  30124  llnle  30154  2atm  30163  ps-2c  30164  lplni2  30173  lplnle  30176  lplnnle2at  30177  lplnri3N  30191  llncvrlpln2  30193  2atmat  30197  2llnjaN  30202  2llnm2N  30204  2llnm4  30206  2llnmeqat  30207  lvolnle3at  30218  4atlem0ae  30230  4atlem0be  30231  4atlem3b  30234  4atlem9  30239  4atlem10a  30240  4atlem10  30242  4atlem11a  30243  4atlem12a  30246  4at  30249  4at2  30250  lplncvrlvol2  30251  2lplnm2N  30257  2llnma1b  30422  2llnma1  30423  2llnma3r  30424  2llnma2  30425  2llnma2rN  30426  cdlema1N  30427  cdlema2N  30428  paddasslem2  30457  paddasslem15  30470  paddasslem16  30471  pmodlem1  30482  pmod2iN  30485  hlmod1i  30492  atmod2i1  30497  atmod2i2  30498  atmod3i1  30500  atmod3i2  30501  atmod4i1  30502  atmod4i2  30503  llnexchb2  30505  dalawlem3  30509  dalawlem4  30510  dalawlem5  30511  dalawlem6  30512  dalawlem7  30513  dalawlem8  30514  dalawlem9  30515  dalawlem11  30517  dalawlem13  30519  dalawlem15  30521  osumcllem7N  30598  osumcllem9N  30600  osumcllem11N  30602  pl42lem1N  30615  4atex  30712  4atex2-0aOLDN  30714  4atex2-0bOLDN  30715  4atex2-0cOLDN  30716  trlval4  30824  cdlemc5  30831  cdlemd5  30838  cdlemd6  30839  cdleme00a  30845  cdleme3g  30870  cdleme3h  30871  cdleme3  30873  cdleme4  30874  cdleme4a  30875  cdleme16aN  30895  cdleme11c  30897  cdleme11g  30901  cdleme11h  30902  cdleme12  30907  cdleme0nex  30926  cdleme18a  30927  cdleme18b  30928  cdleme18c  30929  cdleme18d  30931  cdleme20zN  30937  cdleme20y  30938  cdleme19a  30939  cdleme19b  30940  cdleme19d  30942  cdleme19e  30943  cdleme20aN  30945  cdleme20c  30947  cdleme20d  30948  cdleme20i  30953  cdleme20j  30954  cdleme20l1  30956  cdleme20l2  30957  cdleme20m  30959  cdleme21b  30962  cdleme21c  30963  cdleme21j  30972  cdleme22aa  30975  cdleme22a  30976  cdleme22eALTN  30981  cdleme26e  30995  cdleme26fALTN  30998  cdleme26f  30999  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme27N  31005  cdleme28a  31006  cdleme28b  31007  cdleme30a  31014  cdlemefs45eN  31067  cdleme32c  31079  cdleme32e  31081  cdleme35h  31092  cdleme36a  31096  cdleme36m  31097  cdleme37m  31098  cdleme41sn3aw  31110  cdleme41sn4aw  31111  cdleme41fva11  31113  cdleme42k  31120  cdleme43cN  31127  cdleme43dN  31128  cdleme46f2g1  31130  cdlemeg47rv2  31146  cdlemeg46sfg  31156  cdlemeg46fjgN  31157  cdlemeg46rjgN  31158  cdlemeg46fjv  31159  cdlemeg46frv  31161  cdlemeg46vrg  31163  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemeg46gfv  31166  cdleme50trn2a  31186  cdlemg2fv2  31236  cdlemg4a  31244  cdlemg4e  31250  cdlemg4f  31251  cdlemg8b  31264  cdlemg8c  31265  cdlemg9a  31268  cdlemg9b  31269  cdlemg9  31270  cdlemg10a  31276  cdlemg12a  31279  cdlemg12b  31280  cdlemg12c  31281  cdlemg12  31286  cdlemg17dN  31299  cdlemg17dALTN  31300  cdlemg17e  31301  cdlemg17i  31305  cdlemg17ir  31306  cdlemg17pq  31308  cdlemg17bq  31309  cdlemg17iqN  31310  cdlemg17  31313  cdlemg18b  31315  cdlemg18c  31316  cdlemg18d  31317  cdlemg18  31318  cdlemg19  31320  cdlemg21  31322  cdlemg28a  31329  cdlemg31b0a  31331  cdlemg33b0  31337  cdlemg35  31349  cdlemg44a  31367  cdlemh  31453  cdlemi2  31455  cdlemj1  31457  cdlemk5a  31471  cdlemk5  31472  cdlemki  31477  cdlemkvcl  31478  cdlemk10  31479  cdlemksv2  31483  cdlemk7  31484  cdlemk11  31485  cdlemk12  31486  cdlemk15  31491  cdlemk16a  31492  cdlemk16  31493  cdlemk5u  31497  cdlemk6u  31498  cdlemk18  31504  cdlemk19  31505  cdlemk7u  31506  cdlemk11u  31507  cdlemk12u  31508  cdlemk21N  31509  cdlemk20  31510  cdlemkoatnle-2N  31511  cdlemk13-2N  31512  cdlemkole-2N  31513  cdlemk14-2N  31514  cdlemk15-2N  31515  cdlemk16-2N  31516  cdlemk17-2N  31517  cdlemk18-2N  31522  cdlemk19-2N  31523  cdlemk22  31529  cdlemk30  31530  cdlemk28-3  31544  cdlemk33N  31545  cdlemkfid1N  31557  cdlemkid1  31558  cdlemky  31562  cdlemk11ta  31565  cdlemk35s-id  31574  cdlemk39s-id  31576  cdlemk47  31585  cdlemk48  31586  cdlemk49  31587  cdlemk50  31588  cdlemk51  31589  cdlemk52  31590  cdlemk53a  31591  cdlemk53b  31592  cdlemk53  31593  cdlemk54  31594  cdlemk55a  31595  cdlemkyyN  31598  cdlemk43N  31599  cdlemk55u1  31601  cdlemk55u  31602  cdlemk39u1  31603  cdlemk19u1  31605  cdleml1N  31612  cdleml2N  31613  cdleml3N  31614  dia2dimlem6  31706  cdlemn2  31832  cdlemn2a  31833  cdlemn5pre  31837  cdlemn11pre  31847  dihjustlem  31853  dihjust  31854  dihmeetlem15N  31958  lclkrlem2y  32168
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator