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  6576  elfiun  7179  cofsmo  7891  modexp  11232  iscatd2  13579  funcoppc  13745  funcres  13766  catcisolem  13934  1stfcl  13967  2ndfcl  13968  prfcl  13973  evlfcl  13992  curf1cl  13998  curfcl  14002  hofcl  14029  meetle  14130  prdsxmetlem  17928  isosctrlem3  20116  isosctr  20117  colinearalg  23948  ax5seglem6  23972  ax5seg  23976  axpasch  23979  axeuclid  24001  cgrtr  24025  cgrtr3  24027  ofscom  24040  btwnxfr  24089  colinearxfr  24108  lineext  24109  brofs2  24110  brifs2  24111  fscgr  24113  linecgr  24114  btwnconn1lem1  24120  btwnconn1lem2  24121  btwnconn1lem3  24122  btwnconn1lem4  24123  btwnconn1lem5  24124  btwnconn1lem6  24125  btwnconn1lem7  24126  seglecgr12im  24143  seglecgr12  24144  segletr  24147  broutsideof3  24159  outsideofeq  24163  lineunray  24180  cmpmorass  25377  bisig0  25473  elhaltdp  25478  bnj966  28255  bnj967  28256  eqlkr  28568  omlmod1i2N  28729  cvrcmp2  28753  cvlexch2  28798  cvlexchb2  28800  cvlatexchb2  28804  cvlatexch1  28805  cvlatexch2  28806  cvlatexch3  28807  cvlsupr7  28817  cvlsupr8  28818  atnlej1  28847  atnlej2  28848  2llnneN  28877  cvratlem  28889  atcvrneN  28898  atcvrj1  28899  atlelt  28906  2atjm  28913  3noncolr2  28917  3noncolr1N  28918  hlatcon2  28920  3dimlem2  28927  3dim1  28935  3dim2  28936  1cvrat  28944  ps-1  28945  ps-2  28946  2atjlej  28947  hlatexch3N  28948  ps-2b  28950  3atlem1  28951  3atlem2  28952  3atlem6  28956  llnle  28986  2atm  28995  ps-2c  28996  lplni2  29005  lplnle  29008  lplnnle2at  29009  lplnri3N  29023  llncvrlpln2  29025  2atmat  29029  2llnjaN  29034  2llnm2N  29036  2llnm4  29038  2llnmeqat  29039  lvolnle3at  29050  4atlem0ae  29062  4atlem0be  29063  4atlem3b  29066  4atlem9  29071  4atlem10a  29072  4atlem10  29074  4atlem11a  29075  4atlem12a  29078  4at  29081  4at2  29082  lplncvrlvol2  29083  2lplnm2N  29089  2llnma1b  29254  2llnma1  29255  2llnma3r  29256  2llnma2  29257  2llnma2rN  29258  cdlema1N  29259  cdlema2N  29260  paddasslem2  29289  paddasslem15  29302  paddasslem16  29303  pmodlem1  29314  pmod2iN  29317  hlmod1i  29324  atmod2i1  29329  atmod2i2  29330  atmod3i1  29332  atmod3i2  29333  atmod4i1  29334  atmod4i2  29335  llnexchb2  29337  dalawlem3  29341  dalawlem4  29342  dalawlem5  29343  dalawlem6  29344  dalawlem7  29345  dalawlem8  29346  dalawlem9  29347  dalawlem11  29349  dalawlem13  29351  dalawlem15  29353  osumcllem7N  29430  osumcllem9N  29432  osumcllem11N  29434  pl42lem1N  29447  4atex  29544  4atex2-0aOLDN  29546  4atex2-0bOLDN  29547  4atex2-0cOLDN  29548  trlval4  29656  cdlemc5  29663  cdlemd5  29670  cdlemd6  29671  cdleme00a  29677  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme4a  29707  cdleme16aN  29727  cdleme11c  29729  cdleme11g  29733  cdleme11h  29734  cdleme12  29739  cdleme0nex  29758  cdleme18a  29759  cdleme18b  29760  cdleme18c  29761  cdleme18d  29763  cdleme20zN  29769  cdleme20y  29770  cdleme19a  29771  cdleme19b  29772  cdleme19d  29774  cdleme19e  29775  cdleme20aN  29777  cdleme20c  29779  cdleme20d  29780  cdleme20i  29785  cdleme20j  29786  cdleme20l1  29788  cdleme20l2  29789  cdleme20m  29791  cdleme21b  29794  cdleme21c  29795  cdleme21j  29804  cdleme22aa  29807  cdleme22a  29808  cdleme22eALTN  29813  cdleme26e  29827  cdleme26fALTN  29830  cdleme26f  29831  cdleme26f2ALTN  29832  cdleme26f2  29833  cdleme27N  29837  cdleme28a  29838  cdleme28b  29839  cdleme30a  29846  cdlemefs45eN  29899  cdleme32c  29911  cdleme32e  29913  cdleme35h  29924  cdleme36a  29928  cdleme36m  29929  cdleme37m  29930  cdleme41sn3aw  29942  cdleme41sn4aw  29943  cdleme41fva11  29945  cdleme42k  29952  cdleme43cN  29959  cdleme43dN  29960  cdleme46f2g1  29962  cdlemeg47rv2  29978  cdlemeg46sfg  29988  cdlemeg46fjgN  29989  cdlemeg46rjgN  29990  cdlemeg46fjv  29991  cdlemeg46frv  29993  cdlemeg46vrg  29995  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemeg46gfv  29998  cdleme50trn2a  30018  cdlemg2fv2  30068  cdlemg4a  30076  cdlemg4e  30082  cdlemg4f  30083  cdlemg8b  30096  cdlemg8c  30097  cdlemg9a  30100  cdlemg9b  30101  cdlemg9  30102  cdlemg10a  30108  cdlemg12a  30111  cdlemg12b  30112  cdlemg12c  30113  cdlemg12  30118  cdlemg17dN  30131  cdlemg17dALTN  30132  cdlemg17e  30133  cdlemg17i  30137  cdlemg17ir  30138  cdlemg17pq  30140  cdlemg17bq  30141  cdlemg17iqN  30142  cdlemg17  30145  cdlemg18b  30147  cdlemg18c  30148  cdlemg18d  30149  cdlemg18  30150  cdlemg19  30152  cdlemg21  30154  cdlemg28a  30161  cdlemg31b0a  30163  cdlemg33b0  30169  cdlemg35  30181  cdlemg44a  30199  cdlemh  30285  cdlemi2  30287  cdlemj1  30289  cdlemk5a  30303  cdlemk5  30304  cdlemki  30309  cdlemkvcl  30310  cdlemk10  30311  cdlemksv2  30315  cdlemk7  30316  cdlemk11  30317  cdlemk12  30318  cdlemk15  30323  cdlemk16a  30324  cdlemk16  30325  cdlemk5u  30329  cdlemk6u  30330  cdlemk18  30336  cdlemk19  30337  cdlemk7u  30338  cdlemk11u  30339  cdlemk12u  30340  cdlemk21N  30341  cdlemk20  30342  cdlemkoatnle-2N  30343  cdlemk13-2N  30344  cdlemkole-2N  30345  cdlemk14-2N  30346  cdlemk15-2N  30347  cdlemk16-2N  30348  cdlemk17-2N  30349  cdlemk18-2N  30354  cdlemk19-2N  30355  cdlemk22  30361  cdlemk30  30362  cdlemk28-3  30376  cdlemk33N  30377  cdlemkfid1N  30389  cdlemkid1  30390  cdlemky  30394  cdlemk11ta  30397  cdlemk35s-id  30406  cdlemk39s-id  30408  cdlemk47  30417  cdlemk48  30418  cdlemk49  30419  cdlemk50  30420  cdlemk51  30421  cdlemk52  30422  cdlemk53a  30423  cdlemk53b  30424  cdlemk53  30425  cdlemk54  30426  cdlemk55a  30427  cdlemkyyN  30430  cdlemk43N  30431  cdlemk55u1  30433  cdlemk55u  30434  cdlemk39u1  30435  cdlemk19u1  30437  cdleml1N  30444  cdleml2N  30445  cdleml3N  30446  dia2dimlem6  30538  cdlemn2  30664  cdlemn2a  30665  cdlemn5pre  30669  cdlemn11pre  30679  dihjustlem  30685  dihjust  30686  dihmeetlem15N  30790  lclkrlem2y  31000
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