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

Theorem simp21 988
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp21  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )

Proof of Theorem simp21
StepHypRef Expression
1 simp1 955 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl21  1033  simpr21  1042  simp121  1087  simp221  1096  simp321  1105  omeulem1  6576  cofsmo  7891  axdc4lem  8077  0catg  13585  funcoppc  13745  funcres  13766  catcisolem  13934  1stfcl  13967  2ndfcl  13968  prfcl  13973  evlfcl  13992  curf1cl  13998  curfcl  14002  hofcl  14029  meetle  14130  mulgdirlem  14587  prdsxmetlem  17928  isosctrlem3  20116  isosctr  20117  amgmlem  20280  colinearalg  23948  ax5seglem6  23972  ax5seg  23976  axpasch  23979  axeuclidlem  24000  axeuclid  24001  cgrtr  24025  cgrtr3  24027  ofscom  24040  segconeq  24043  ifscgr  24077  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  lineelsb2  24181  linecom  24183  cmpmorass  25377  bisig0  25473  isig1a2  25474  bnj1128  28299  lshpkrlem5  28583  omlmod1i2N  28729  cvrnbtwn3  28745  cvrcmp  28752  cvrcmp2  28753  cvlexch2  28798  cvlexchb2  28800  cvlatexchb2  28804  cvlatexch2  28806  cvlatexch3  28807  cvlsupr7  28817  atnlej1  28847  atnlej2  28848  2llnneN  28877  cvratlem  28889  atcvrneN  28898  atcvrj1  28899  atlelt  28906  2atjm  28913  3noncolr2  28917  3noncolr1N  28918  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  3atlem5  28955  3atlem6  28956  llnle  28986  2atm  28995  ps-2c  28996  lplni2  29005  lplnle  29008  lplnnle2at  29009  lplnri3N  29023  llncvrlpln2  29025  2atmat  29029  2llnm2N  29036  2llnm4  29038  2llnmeqat  29039  lvolnle3at  29050  4atlem0ae  29062  4atlem0be  29063  4atlem3b  29066  4atlem9  29071  4atlem10a  29072  4atlem10  29074  4atlem11a  29075  4atlem12a  29078  4at2  29082  2lplnm2N  29089  lneq2at  29246  2llnma1b  29254  2llnma1  29255  2llnma3r  29256  2llnma2  29257  2llnma2rN  29258  cdlema1N  29259  paddasslem2  29289  paddasslem15  29302  paddasslem16  29303  pmodlem1  29314  pmodlem2  29315  pmod2iN  29317  hlmod1i  29324  atmod1i1m  29326  atmod2i1  29329  atmod2i2  29330  atmod3i1  29332  atmod3i2  29333  atmod4i1  29334  atmod4i2  29335  llnexchb2lem  29336  llnexch2N  29338  dalawlem3  29341  dalawlem4  29342  dalawlem5  29343  dalawlem6  29344  dalawlem7  29345  dalawlem8  29346  dalawlem9  29347  dalawlem11  29349  dalawlem12  29350  dalawlem13  29351  dalawlem15  29353  osumcllem9N  29432  pl42lem1N  29447  4atexlems  29520  4atex2  29545  4atex2-0bOLDN  29547  trlval4  29656  cdlemc5  29663  cdlemc6  29664  cdlemd2  29667  cdlemd4  29669  cdlemd6  29671  cdleme00a  29677  cdleme0e  29685  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme4a  29707  cdleme5  29708  cdleme9  29721  cdleme16aN  29727  cdleme11c  29729  cdleme11e  29731  cdleme11g  29733  cdleme11h  29734  cdleme11j  29735  cdleme11k  29736  cdleme11l  29737  cdleme11  29738  cdleme12  29739  cdleme14  29741  cdleme15c  29744  cdleme16b  29747  cdleme16c  29748  cdleme16d  29749  cdleme16e  29750  cdleme16f  29751  cdleme0nex  29758  cdleme18a  29759  cdleme18c  29761  cdleme18d  29763  cdlemednpq  29767  cdlemednuN  29768  cdleme20zN  29769  cdleme20y  29770  cdleme19a  29771  cdleme19b  29772  cdleme19d  29774  cdleme19e  29775  cdleme20aN  29777  cdleme20bN  29778  cdleme20c  29779  cdleme20d  29780  cdleme20f  29782  cdleme20g  29783  cdleme20i  29785  cdleme20j  29786  cdleme20l1  29788  cdleme20l2  29789  cdleme20l  29790  cdleme20m  29791  cdleme21b  29794  cdleme21c  29795  cdleme21e  29799  cdleme21f  29800  cdleme22a  29808  cdleme22b  29809  cdleme22e  29812  cdleme22eALTN  29813  cdleme22f  29814  cdleme26eALTN  29829  cdleme26fALTN  29830  cdleme26f  29831  cdleme26f2ALTN  29832  cdleme26f2  29833  cdleme27N  29837  cdleme28a  29838  cdleme28b  29839  cdleme30a  29846  cdleme43fsv1snlem  29888  cdlemefs31fv1  29892  cdlemefs45eN  29899  cdleme32b  29910  cdleme32c  29911  cdleme32d  29912  cdleme35h  29924  cdleme36a  29928  cdleme36m  29929  cdleme37m  29930  cdleme40m  29935  cdleme40n  29936  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  cdlemg4a  30076  cdlemg4d  30081  cdlemg4e  30082  cdlemg4f  30083  cdlemg4g  30084  cdlemg4  30085  cdlemg6d  30089  cdlemg6e  30090  cdlemg8b  30096  cdlemg8c  30097  cdlemg9a  30100  cdlemg9b  30101  cdlemg10a  30108  cdlemg10  30109  cdlemg12a  30111  cdlemg12b  30112  cdlemg12f  30116  cdlemg12g  30117  cdlemg12  30118  cdlemg17dN  30131  cdlemg17dALTN  30132  cdlemg17e  30133  cdlemg17f  30134  cdlemg17g  30135  cdlemg17h  30136  cdlemg17i  30137  cdlemg17pq  30140  cdlemg17iqN  30142  cdlemg17  30145  cdlemg18b  30147  cdlemg18c  30148  cdlemg19a  30151  cdlemg19  30152  cdlemg28a  30161  cdlemg27b  30164  cdlemg28b  30171  cdlemg28  30172  cdlemg33a  30174  cdlemg33b  30175  cdlemg33c  30176  cdlemg33d  30177  cdlemg33e  30178  cdlemg33  30179  cdlemg35  30181  cdlemg36  30182  cdlemg44a  30199  cdlemh  30285  cdlemi2  30287  cdlemj1  30289  tendocan  30292  cdlemk5a  30303  cdlemki  30309  cdlemkvcl  30310  cdlemk10  30311  cdlemksv2  30315  cdlemkole  30321  cdlemk14  30322  cdlemk15  30323  cdlemk16a  30324  cdlemk16  30325  cdlemk17  30326  cdlemk18  30336  cdlemk19  30337  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  cdlemk30  30362  cdlemk18-3N  30368  cdlemk23-3  30370  cdlemk25-3  30372  cdlemk27-3  30375  cdlemk37  30382  cdlemkfid1N  30389  cdlemkid1  30390  cdlemky  30394  cdlemk11ta  30397  cdlemk47  30417  cdlemk48  30418  cdlemk49  30419  cdlemk50  30420  cdlemk51  30421  cdlemk52  30422  cdlemk53a  30423  cdlemk54  30426  cdlemk39u1  30435  cdlemk19u1  30437  cdleml1N  30444  cdleml2N  30445  cdleml3N  30446  dia2dimlem6  30538  cdlemn2  30664  cdlemn2a  30665  cdlemn5pre  30669  cdlemn10  30675  cdlemn11c  30678  cdlemn11pre  30679  dihjustlem  30685  dihjust  30686  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