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  5441  omeulem1  6761  elfiun  7370  cofsmo  8082  modexp  11441  iscatd2  13833  funcoppc  13999  funcres  14020  catcisolem  14188  1stfcl  14221  2ndfcl  14222  prfcl  14227  evlfcl  14246  curf1cl  14252  curfcl  14256  hofcl  14283  meetle  14384  prdsxmetlem  18306  isosctrlem3  20531  isosctr  20532  rhmdvd  24075  colinearalg  25563  ax5seglem6  25587  ax5seg  25591  axpasch  25594  axeuclid  25616  cgrtr  25640  cgrtr3  25642  ofscom  25655  btwnxfr  25704  colinearxfr  25723  lineext  25724  brofs2  25725  brifs2  25726  fscgr  25728  linecgr  25729  btwnconn1lem1  25735  btwnconn1lem2  25736  btwnconn1lem3  25737  btwnconn1lem4  25738  btwnconn1lem5  25739  btwnconn1lem6  25740  btwnconn1lem7  25741  seglecgr12im  25758  seglecgr12  25759  segletr  25762  broutsideof3  25774  outsideofeq  25778  lineunray  25795  bnj966  28653  bnj967  28654  eqlkr  29214  omlmod1i2N  29375  cvrcmp2  29399  cvlexch2  29444  cvlexchb2  29446  cvlatexchb2  29450  cvlatexch1  29451  cvlatexch2  29452  cvlatexch3  29453  cvlsupr7  29463  cvlsupr8  29464  atnlej1  29493  atnlej2  29494  2llnneN  29523  cvratlem  29535  atcvrneN  29544  atcvrj1  29545  atlelt  29552  2atjm  29559  3noncolr2  29563  3noncolr1N  29564  hlatcon2  29566  3dimlem2  29573  3dim1  29581  3dim2  29582  1cvrat  29590  ps-1  29591  ps-2  29592  2atjlej  29593  hlatexch3N  29594  ps-2b  29596  3atlem1  29597  3atlem2  29598  3atlem6  29602  llnle  29632  2atm  29641  ps-2c  29642  lplni2  29651  lplnle  29654  lplnnle2at  29655  lplnri3N  29669  llncvrlpln2  29671  2atmat  29675  2llnjaN  29680  2llnm2N  29682  2llnm4  29684  2llnmeqat  29685  lvolnle3at  29696  4atlem0ae  29708  4atlem0be  29709  4atlem3b  29712  4atlem9  29717  4atlem10a  29718  4atlem10  29720  4atlem11a  29721  4atlem12a  29724  4at  29727  4at2  29728  lplncvrlvol2  29729  2lplnm2N  29735  2llnma1b  29900  2llnma1  29901  2llnma3r  29902  2llnma2  29903  2llnma2rN  29904  cdlema1N  29905  cdlema2N  29906  paddasslem2  29935  paddasslem15  29948  paddasslem16  29949  pmodlem1  29960  pmod2iN  29963  hlmod1i  29970  atmod2i1  29975  atmod2i2  29976  atmod3i1  29978  atmod3i2  29979  atmod4i1  29980  atmod4i2  29981  llnexchb2  29983  dalawlem3  29987  dalawlem4  29988  dalawlem5  29989  dalawlem6  29990  dalawlem7  29991  dalawlem8  29992  dalawlem9  29993  dalawlem11  29995  dalawlem13  29997  dalawlem15  29999  osumcllem7N  30076  osumcllem9N  30078  osumcllem11N  30080  pl42lem1N  30093  4atex  30190  4atex2-0aOLDN  30192  4atex2-0bOLDN  30193  4atex2-0cOLDN  30194  trlval4  30302  cdlemc5  30309  cdlemd5  30316  cdlemd6  30317  cdleme00a  30323  cdleme3g  30348  cdleme3h  30349  cdleme3  30351  cdleme4  30352  cdleme4a  30353  cdleme16aN  30373  cdleme11c  30375  cdleme11g  30379  cdleme11h  30380  cdleme12  30385  cdleme0nex  30404  cdleme18a  30405  cdleme18b  30406  cdleme18c  30407  cdleme18d  30409  cdleme20zN  30415  cdleme20y  30416  cdleme19a  30417  cdleme19b  30418  cdleme19d  30420  cdleme19e  30421  cdleme20aN  30423  cdleme20c  30425  cdleme20d  30426  cdleme20i  30431  cdleme20j  30432  cdleme20l1  30434  cdleme20l2  30435  cdleme20m  30437  cdleme21b  30440  cdleme21c  30441  cdleme21j  30450  cdleme22aa  30453  cdleme22a  30454  cdleme22eALTN  30459  cdleme26e  30473  cdleme26fALTN  30476  cdleme26f  30477  cdleme26f2ALTN  30478  cdleme26f2  30479  cdleme27N  30483  cdleme28a  30484  cdleme28b  30485  cdleme30a  30492  cdlemefs45eN  30545  cdleme32c  30557  cdleme32e  30559  cdleme35h  30570  cdleme36a  30574  cdleme36m  30575  cdleme37m  30576  cdleme41sn3aw  30588  cdleme41sn4aw  30589  cdleme41fva11  30591  cdleme42k  30598  cdleme43cN  30605  cdleme43dN  30606  cdleme46f2g1  30608  cdlemeg47rv2  30624  cdlemeg46sfg  30634  cdlemeg46fjgN  30635  cdlemeg46rjgN  30636  cdlemeg46fjv  30637  cdlemeg46frv  30639  cdlemeg46vrg  30641  cdlemeg46rgv  30642  cdlemeg46req  30643  cdlemeg46gfv  30644  cdleme50trn2a  30664  cdlemg2fv2  30714  cdlemg4a  30722  cdlemg4e  30728  cdlemg4f  30729  cdlemg8b  30742  cdlemg8c  30743  cdlemg9a  30746  cdlemg9b  30747  cdlemg9  30748  cdlemg10a  30754  cdlemg12a  30757  cdlemg12b  30758  cdlemg12c  30759  cdlemg12  30764  cdlemg17dN  30777  cdlemg17dALTN  30778  cdlemg17e  30779  cdlemg17i  30783  cdlemg17ir  30784  cdlemg17pq  30786  cdlemg17bq  30787  cdlemg17iqN  30788  cdlemg17  30791  cdlemg18b  30793  cdlemg18c  30794  cdlemg18d  30795  cdlemg18  30796  cdlemg19  30798  cdlemg21  30800  cdlemg28a  30807  cdlemg31b0a  30809  cdlemg33b0  30815  cdlemg35  30827  cdlemg44a  30845  cdlemh  30931  cdlemi2  30933  cdlemj1  30935  cdlemk5a  30949  cdlemk5  30950  cdlemki  30955  cdlemkvcl  30956  cdlemk10  30957  cdlemksv2  30961  cdlemk7  30962  cdlemk11  30963  cdlemk12  30964  cdlemk15  30969  cdlemk16a  30970  cdlemk16  30971  cdlemk5u  30975  cdlemk6u  30976  cdlemk18  30982  cdlemk19  30983  cdlemk7u  30984  cdlemk11u  30985  cdlemk12u  30986  cdlemk21N  30987  cdlemk20  30988  cdlemkoatnle-2N  30989  cdlemk13-2N  30990  cdlemkole-2N  30991  cdlemk14-2N  30992  cdlemk15-2N  30993  cdlemk16-2N  30994  cdlemk17-2N  30995  cdlemk18-2N  31000  cdlemk19-2N  31001  cdlemk22  31007  cdlemk30  31008  cdlemk28-3  31022  cdlemk33N  31023  cdlemkfid1N  31035  cdlemkid1  31036  cdlemky  31040  cdlemk11ta  31043  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk47  31063  cdlemk48  31064  cdlemk49  31065  cdlemk50  31066  cdlemk51  31067  cdlemk52  31068  cdlemk53a  31069  cdlemk53b  31070  cdlemk53  31071  cdlemk54  31072  cdlemk55a  31073  cdlemkyyN  31076  cdlemk43N  31077  cdlemk55u1  31079  cdlemk55u  31080  cdlemk39u1  31081  cdlemk19u1  31083  cdleml1N  31090  cdleml2N  31091  cdleml3N  31092  dia2dimlem6  31184  cdlemn2  31310  cdlemn2a  31311  cdlemn5pre  31315  cdlemn11pre  31325  dihjustlem  31331  dihjust  31332  dihmeetlem15N  31436  lclkrlem2y  31646
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