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

Theorem simp23 993
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 960 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
213ad2ant2 980 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl23  1038  simpr23  1047  simp123  1092  simp223  1101  simp323  1110  funtpg  5536  omeulem1  6861  elfiun  7471  cofsmo  8187  modexp  11552  iscatd2  13944  funcoppc  14110  funcres  14131  catcisolem  14299  1stfcl  14332  2ndfcl  14333  prfcl  14338  evlfcl  14357  curf1cl  14363  curfcl  14367  hofcl  14394  meetle  14495  prdsxmetlem  18436  isosctrlem3  20702  isosctr  20703  rhmdvd  24294  colinearalg  25884  ax5seglem6  25908  ax5seg  25912  axpasch  25915  axeuclid  25937  cgrtr  25961  cgrtr3  25963  ofscom  25976  btwnxfr  26025  colinearxfr  26044  lineext  26045  brofs2  26046  brifs2  26047  fscgr  26049  linecgr  26050  btwnconn1lem1  26056  btwnconn1lem2  26057  btwnconn1lem3  26058  btwnconn1lem4  26059  btwnconn1lem5  26060  btwnconn1lem6  26061  btwnconn1lem7  26062  seglecgr12im  26079  seglecgr12  26080  segletr  26083  broutsideof3  26095  outsideofeq  26099  lineunray  26116  bnj966  29489  bnj967  29490  eqlkr  30071  omlmod1i2N  30232  cvrcmp2  30256  cvlexch2  30301  cvlexchb2  30303  cvlatexchb2  30307  cvlatexch1  30308  cvlatexch2  30309  cvlatexch3  30310  cvlsupr7  30320  cvlsupr8  30321  atnlej1  30350  atnlej2  30351  2llnneN  30380  cvratlem  30392  atcvrneN  30401  atcvrj1  30402  atlelt  30409  2atjm  30416  3noncolr2  30420  3noncolr1N  30421  hlatcon2  30423  3dimlem2  30430  3dim1  30438  3dim2  30439  1cvrat  30447  ps-1  30448  ps-2  30449  2atjlej  30450  hlatexch3N  30451  ps-2b  30453  3atlem1  30454  3atlem2  30455  3atlem6  30459  llnle  30489  2atm  30498  ps-2c  30499  lplni2  30508  lplnle  30511  lplnnle2at  30512  lplnri3N  30526  llncvrlpln2  30528  2atmat  30532  2llnjaN  30537  2llnm2N  30539  2llnm4  30541  2llnmeqat  30542  lvolnle3at  30553  4atlem0ae  30565  4atlem0be  30566  4atlem3b  30569  4atlem9  30574  4atlem10a  30575  4atlem10  30577  4atlem11a  30578  4atlem12a  30581  4at  30584  4at2  30585  lplncvrlvol2  30586  2lplnm2N  30592  2llnma1b  30757  2llnma1  30758  2llnma3r  30759  2llnma2  30760  2llnma2rN  30761  cdlema1N  30762  cdlema2N  30763  paddasslem2  30792  paddasslem15  30805  paddasslem16  30806  pmodlem1  30817  pmod2iN  30820  hlmod1i  30827  atmod2i1  30832  atmod2i2  30833  atmod3i1  30835  atmod3i2  30836  atmod4i1  30837  atmod4i2  30838  llnexchb2  30840  dalawlem3  30844  dalawlem4  30845  dalawlem5  30846  dalawlem6  30847  dalawlem7  30848  dalawlem8  30849  dalawlem9  30850  dalawlem11  30852  dalawlem13  30854  dalawlem15  30856  osumcllem7N  30933  osumcllem9N  30935  osumcllem11N  30937  pl42lem1N  30950  4atex  31047  4atex2-0aOLDN  31049  4atex2-0bOLDN  31050  4atex2-0cOLDN  31051  trlval4  31159  cdlemc5  31166  cdlemd5  31173  cdlemd6  31174  cdleme00a  31180  cdleme3g  31205  cdleme3h  31206  cdleme3  31208  cdleme4  31209  cdleme4a  31210  cdleme16aN  31230  cdleme11c  31232  cdleme11g  31236  cdleme11h  31237  cdleme12  31242  cdleme0nex  31261  cdleme18a  31262  cdleme18b  31263  cdleme18c  31264  cdleme18d  31266  cdleme20zN  31272  cdleme20y  31273  cdleme19a  31274  cdleme19b  31275  cdleme19d  31277  cdleme19e  31278  cdleme20aN  31280  cdleme20c  31282  cdleme20d  31283  cdleme20i  31288  cdleme20j  31289  cdleme20l1  31291  cdleme20l2  31292  cdleme20m  31294  cdleme21b  31297  cdleme21c  31298  cdleme21j  31307  cdleme22aa  31310  cdleme22a  31311  cdleme22eALTN  31316  cdleme26e  31330  cdleme26fALTN  31333  cdleme26f  31334  cdleme26f2ALTN  31335  cdleme26f2  31336  cdleme27N  31340  cdleme28a  31341  cdleme28b  31342  cdleme30a  31349  cdlemefs45eN  31402  cdleme32c  31414  cdleme32e  31416  cdleme35h  31427  cdleme36a  31431  cdleme36m  31432  cdleme37m  31433  cdleme41sn3aw  31445  cdleme41sn4aw  31446  cdleme41fva11  31448  cdleme42k  31455  cdleme43cN  31462  cdleme43dN  31463  cdleme46f2g1  31465  cdlemeg47rv2  31481  cdlemeg46sfg  31491  cdlemeg46fjgN  31492  cdlemeg46rjgN  31493  cdlemeg46fjv  31494  cdlemeg46frv  31496  cdlemeg46vrg  31498  cdlemeg46rgv  31499  cdlemeg46req  31500  cdlemeg46gfv  31501  cdleme50trn2a  31521  cdlemg2fv2  31571  cdlemg4a  31579  cdlemg4e  31585  cdlemg4f  31586  cdlemg8b  31599  cdlemg8c  31600  cdlemg9a  31603  cdlemg9b  31604  cdlemg9  31605  cdlemg10a  31611  cdlemg12a  31614  cdlemg12b  31615  cdlemg12c  31616  cdlemg12  31621  cdlemg17dN  31634  cdlemg17dALTN  31635  cdlemg17e  31636  cdlemg17i  31640  cdlemg17ir  31641  cdlemg17pq  31643  cdlemg17bq  31644  cdlemg17iqN  31645  cdlemg17  31648  cdlemg18b  31650  cdlemg18c  31651  cdlemg18d  31652  cdlemg18  31653  cdlemg19  31655  cdlemg21  31657  cdlemg28a  31664  cdlemg31b0a  31666  cdlemg33b0  31672  cdlemg35  31684  cdlemg44a  31702  cdlemh  31788  cdlemi2  31790  cdlemj1  31792  cdlemk5a  31806  cdlemk5  31807  cdlemki  31812  cdlemkvcl  31813  cdlemk10  31814  cdlemksv2  31818  cdlemk7  31819  cdlemk11  31820  cdlemk12  31821  cdlemk15  31826  cdlemk16a  31827  cdlemk16  31828  cdlemk5u  31832  cdlemk6u  31833  cdlemk18  31839  cdlemk19  31840  cdlemk7u  31841  cdlemk11u  31842  cdlemk12u  31843  cdlemk21N  31844  cdlemk20  31845  cdlemkoatnle-2N  31846  cdlemk13-2N  31847  cdlemkole-2N  31848  cdlemk14-2N  31849  cdlemk15-2N  31850  cdlemk16-2N  31851  cdlemk17-2N  31852  cdlemk18-2N  31857  cdlemk19-2N  31858  cdlemk22  31864  cdlemk30  31865  cdlemk28-3  31879  cdlemk33N  31880  cdlemkfid1N  31892  cdlemkid1  31893  cdlemky  31897  cdlemk11ta  31900  cdlemk35s-id  31909  cdlemk39s-id  31911  cdlemk47  31920  cdlemk48  31921  cdlemk49  31922  cdlemk50  31923  cdlemk51  31924  cdlemk52  31925  cdlemk53a  31926  cdlemk53b  31927  cdlemk53  31928  cdlemk54  31929  cdlemk55a  31930  cdlemkyyN  31933  cdlemk43N  31934  cdlemk55u1  31936  cdlemk55u  31937  cdlemk39u1  31938  cdlemk19u1  31940  cdleml1N  31947  cdleml2N  31948  cdleml3N  31949  dia2dimlem6  32041  cdlemn2  32167  cdlemn2a  32168  cdlemn5pre  32172  cdlemn11pre  32182  dihjustlem  32188  dihjust  32189  dihmeetlem15N  32293  lclkrlem2y  32503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator