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

Theorem simp21 991
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
213ad2ant2 980 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl21  1036  simpr21  1045  simp121  1090  simp221  1099  simp321  1108  omeulem1  6861  cofsmo  8187  axdc4lem  8373  0catg  13950  funcoppc  14110  funcres  14131  catcisolem  14299  1stfcl  14332  2ndfcl  14333  prfcl  14338  evlfcl  14357  curf1cl  14363  curfcl  14367  hofcl  14394  meetle  14495  mulgdirlem  14952  prdsxmetlem  18436  isosctrlem3  20702  isosctr  20703  amgmlem  20866  ofldaddlt  24276  rhmdvd  24294  colinearalg  25884  ax5seglem6  25908  ax5seg  25912  axpasch  25915  axeuclidlem  25936  axeuclid  25937  cgrtr  25961  cgrtr3  25963  ofscom  25976  segconeq  25979  ifscgr  26013  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  lineelsb2  26117  linecom  26119  bnj1128  29533  lshpkrlem5  30086  omlmod1i2N  30232  cvrnbtwn3  30248  cvrcmp  30255  cvrcmp2  30256  cvlexch2  30301  cvlexchb2  30303  cvlatexchb2  30307  cvlatexch2  30309  cvlatexch3  30310  cvlsupr7  30320  atnlej1  30350  atnlej2  30351  2llnneN  30380  cvratlem  30392  atcvrneN  30401  atcvrj1  30402  atlelt  30409  2atjm  30416  3noncolr2  30420  3noncolr1N  30421  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  3atlem5  30458  3atlem6  30459  llnle  30489  2atm  30498  ps-2c  30499  lplni2  30508  lplnle  30511  lplnnle2at  30512  lplnri3N  30526  llncvrlpln2  30528  2atmat  30532  2llnm2N  30539  2llnm4  30541  2llnmeqat  30542  lvolnle3at  30553  4atlem0ae  30565  4atlem0be  30566  4atlem3b  30569  4atlem9  30574  4atlem10a  30575  4atlem10  30577  4atlem11a  30578  4atlem12a  30581  4at2  30585  2lplnm2N  30592  lneq2at  30749  2llnma1b  30757  2llnma1  30758  2llnma3r  30759  2llnma2  30760  2llnma2rN  30761  cdlema1N  30762  paddasslem2  30792  paddasslem15  30805  paddasslem16  30806  pmodlem1  30817  pmodlem2  30818  pmod2iN  30820  hlmod1i  30827  atmod1i1m  30829  atmod2i1  30832  atmod2i2  30833  atmod3i1  30835  atmod3i2  30836  atmod4i1  30837  atmod4i2  30838  llnexchb2lem  30839  llnexch2N  30841  dalawlem3  30844  dalawlem4  30845  dalawlem5  30846  dalawlem6  30847  dalawlem7  30848  dalawlem8  30849  dalawlem9  30850  dalawlem11  30852  dalawlem12  30853  dalawlem13  30854  dalawlem15  30856  osumcllem9N  30935  pl42lem1N  30950  4atexlems  31023  4atex2  31048  4atex2-0bOLDN  31050  trlval4  31159  cdlemc5  31166  cdlemc6  31167  cdlemd2  31170  cdlemd4  31172  cdlemd6  31174  cdleme00a  31180  cdleme0e  31188  cdleme3g  31205  cdleme3h  31206  cdleme3  31208  cdleme4  31209  cdleme4a  31210  cdleme5  31211  cdleme9  31224  cdleme16aN  31230  cdleme11c  31232  cdleme11e  31234  cdleme11g  31236  cdleme11h  31237  cdleme11j  31238  cdleme11k  31239  cdleme11l  31240  cdleme11  31241  cdleme12  31242  cdleme14  31244  cdleme15c  31247  cdleme16b  31250  cdleme16c  31251  cdleme16d  31252  cdleme16e  31253  cdleme16f  31254  cdleme0nex  31261  cdleme18a  31262  cdleme18c  31264  cdleme18d  31266  cdlemednpq  31270  cdlemednuN  31271  cdleme20zN  31272  cdleme20y  31273  cdleme19a  31274  cdleme19b  31275  cdleme19d  31277  cdleme19e  31278  cdleme20aN  31280  cdleme20bN  31281  cdleme20c  31282  cdleme20d  31283  cdleme20f  31285  cdleme20g  31286  cdleme20i  31288  cdleme20j  31289  cdleme20l1  31291  cdleme20l2  31292  cdleme20l  31293  cdleme20m  31294  cdleme21b  31297  cdleme21c  31298  cdleme21e  31302  cdleme21f  31303  cdleme22a  31311  cdleme22b  31312  cdleme22e  31315  cdleme22eALTN  31316  cdleme22f  31317  cdleme26eALTN  31332  cdleme26fALTN  31333  cdleme26f  31334  cdleme26f2ALTN  31335  cdleme26f2  31336  cdleme27N  31340  cdleme28a  31341  cdleme28b  31342  cdleme30a  31349  cdleme43fsv1snlem  31391  cdlemefs31fv1  31395  cdlemefs45eN  31402  cdleme32b  31413  cdleme32c  31414  cdleme32d  31415  cdleme35h  31427  cdleme36a  31431  cdleme36m  31432  cdleme37m  31433  cdleme40m  31438  cdleme40n  31439  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  cdlemg4a  31579  cdlemg4d  31584  cdlemg4e  31585  cdlemg4f  31586  cdlemg4g  31587  cdlemg4  31588  cdlemg6d  31592  cdlemg6e  31593  cdlemg8b  31599  cdlemg8c  31600  cdlemg9a  31603  cdlemg9b  31604  cdlemg10a  31611  cdlemg10  31612  cdlemg12a  31614  cdlemg12b  31615  cdlemg12f  31619  cdlemg12g  31620  cdlemg12  31621  cdlemg17dN  31634  cdlemg17dALTN  31635  cdlemg17e  31636  cdlemg17f  31637  cdlemg17g  31638  cdlemg17h  31639  cdlemg17i  31640  cdlemg17pq  31643  cdlemg17iqN  31645  cdlemg17  31648  cdlemg18b  31650  cdlemg18c  31651  cdlemg19a  31654  cdlemg19  31655  cdlemg28a  31664  cdlemg27b  31667  cdlemg28b  31674  cdlemg28  31675  cdlemg33a  31677  cdlemg33b  31678  cdlemg33c  31679  cdlemg33d  31680  cdlemg33e  31681  cdlemg33  31682  cdlemg35  31684  cdlemg36  31685  cdlemg44a  31702  cdlemh  31788  cdlemi2  31790  cdlemj1  31792  tendocan  31795  cdlemk5a  31806  cdlemki  31812  cdlemkvcl  31813  cdlemk10  31814  cdlemksv2  31818  cdlemkole  31824  cdlemk14  31825  cdlemk15  31826  cdlemk16a  31827  cdlemk16  31828  cdlemk17  31829  cdlemk18  31839  cdlemk19  31840  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  cdlemk30  31865  cdlemk18-3N  31871  cdlemk23-3  31873  cdlemk25-3  31875  cdlemk27-3  31878  cdlemk37  31885  cdlemkfid1N  31892  cdlemkid1  31893  cdlemky  31897  cdlemk11ta  31900  cdlemk47  31920  cdlemk48  31921  cdlemk49  31922  cdlemk50  31923  cdlemk51  31924  cdlemk52  31925  cdlemk53a  31926  cdlemk54  31929  cdlemk39u1  31938  cdlemk19u1  31940  cdleml1N  31947  cdleml2N  31948  cdleml3N  31949  dia2dimlem6  32041  cdlemn2  32167  cdlemn2a  32168  cdlemn5pre  32172  cdlemn10  32178  cdlemn11c  32181  cdlemn11pre  32182  dihjustlem  32188  dihjust  32189  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