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

Theorem simp21 990
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl21  1035  simpr21  1044  simp121  1089  simp221  1098  simp321  1107  omeulem1  6761  cofsmo  8082  axdc4lem  8268  0catg  13839  funcoppc  13999  funcres  14020  catcisolem  14188  1stfcl  14221  2ndfcl  14222  prfcl  14227  evlfcl  14246  curf1cl  14252  curfcl  14256  hofcl  14283  meetle  14384  mulgdirlem  14841  prdsxmetlem  18306  isosctrlem3  20531  isosctr  20532  amgmlem  20695  ofldaddlt  24067  rhmdvd  24075  colinearalg  25563  ax5seglem6  25587  ax5seg  25591  axpasch  25594  axeuclidlem  25615  axeuclid  25616  cgrtr  25640  cgrtr3  25642  ofscom  25655  segconeq  25658  ifscgr  25692  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  lineelsb2  25796  linecom  25798  bnj1128  28697  lshpkrlem5  29229  omlmod1i2N  29375  cvrnbtwn3  29391  cvrcmp  29398  cvrcmp2  29399  cvlexch2  29444  cvlexchb2  29446  cvlatexchb2  29450  cvlatexch2  29452  cvlatexch3  29453  cvlsupr7  29463  atnlej1  29493  atnlej2  29494  2llnneN  29523  cvratlem  29535  atcvrneN  29544  atcvrj1  29545  atlelt  29552  2atjm  29559  3noncolr2  29563  3noncolr1N  29564  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  3atlem5  29601  3atlem6  29602  llnle  29632  2atm  29641  ps-2c  29642  lplni2  29651  lplnle  29654  lplnnle2at  29655  lplnri3N  29669  llncvrlpln2  29671  2atmat  29675  2llnm2N  29682  2llnm4  29684  2llnmeqat  29685  lvolnle3at  29696  4atlem0ae  29708  4atlem0be  29709  4atlem3b  29712  4atlem9  29717  4atlem10a  29718  4atlem10  29720  4atlem11a  29721  4atlem12a  29724  4at2  29728  2lplnm2N  29735  lneq2at  29892  2llnma1b  29900  2llnma1  29901  2llnma3r  29902  2llnma2  29903  2llnma2rN  29904  cdlema1N  29905  paddasslem2  29935  paddasslem15  29948  paddasslem16  29949  pmodlem1  29960  pmodlem2  29961  pmod2iN  29963  hlmod1i  29970  atmod1i1m  29972  atmod2i1  29975  atmod2i2  29976  atmod3i1  29978  atmod3i2  29979  atmod4i1  29980  atmod4i2  29981  llnexchb2lem  29982  llnexch2N  29984  dalawlem3  29987  dalawlem4  29988  dalawlem5  29989  dalawlem6  29990  dalawlem7  29991  dalawlem8  29992  dalawlem9  29993  dalawlem11  29995  dalawlem12  29996  dalawlem13  29997  dalawlem15  29999  osumcllem9N  30078  pl42lem1N  30093  4atexlems  30166  4atex2  30191  4atex2-0bOLDN  30193  trlval4  30302  cdlemc5  30309  cdlemc6  30310  cdlemd2  30313  cdlemd4  30315  cdlemd6  30317  cdleme00a  30323  cdleme0e  30331  cdleme3g  30348  cdleme3h  30349  cdleme3  30351  cdleme4  30352  cdleme4a  30353  cdleme5  30354  cdleme9  30367  cdleme16aN  30373  cdleme11c  30375  cdleme11e  30377  cdleme11g  30379  cdleme11h  30380  cdleme11j  30381  cdleme11k  30382  cdleme11l  30383  cdleme11  30384  cdleme12  30385  cdleme14  30387  cdleme15c  30390  cdleme16b  30393  cdleme16c  30394  cdleme16d  30395  cdleme16e  30396  cdleme16f  30397  cdleme0nex  30404  cdleme18a  30405  cdleme18c  30407  cdleme18d  30409  cdlemednpq  30413  cdlemednuN  30414  cdleme20zN  30415  cdleme20y  30416  cdleme19a  30417  cdleme19b  30418  cdleme19d  30420  cdleme19e  30421  cdleme20aN  30423  cdleme20bN  30424  cdleme20c  30425  cdleme20d  30426  cdleme20f  30428  cdleme20g  30429  cdleme20i  30431  cdleme20j  30432  cdleme20l1  30434  cdleme20l2  30435  cdleme20l  30436  cdleme20m  30437  cdleme21b  30440  cdleme21c  30441  cdleme21e  30445  cdleme21f  30446  cdleme22a  30454  cdleme22b  30455  cdleme22e  30458  cdleme22eALTN  30459  cdleme22f  30460  cdleme26eALTN  30475  cdleme26fALTN  30476  cdleme26f  30477  cdleme26f2ALTN  30478  cdleme26f2  30479  cdleme27N  30483  cdleme28a  30484  cdleme28b  30485  cdleme30a  30492  cdleme43fsv1snlem  30534  cdlemefs31fv1  30538  cdlemefs45eN  30545  cdleme32b  30556  cdleme32c  30557  cdleme32d  30558  cdleme35h  30570  cdleme36a  30574  cdleme36m  30575  cdleme37m  30576  cdleme40m  30581  cdleme40n  30582  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  cdlemg4a  30722  cdlemg4d  30727  cdlemg4e  30728  cdlemg4f  30729  cdlemg4g  30730  cdlemg4  30731  cdlemg6d  30735  cdlemg6e  30736  cdlemg8b  30742  cdlemg8c  30743  cdlemg9a  30746  cdlemg9b  30747  cdlemg10a  30754  cdlemg10  30755  cdlemg12a  30757  cdlemg12b  30758  cdlemg12f  30762  cdlemg12g  30763  cdlemg12  30764  cdlemg17dN  30777  cdlemg17dALTN  30778  cdlemg17e  30779  cdlemg17f  30780  cdlemg17g  30781  cdlemg17h  30782  cdlemg17i  30783  cdlemg17pq  30786  cdlemg17iqN  30788  cdlemg17  30791  cdlemg18b  30793  cdlemg18c  30794  cdlemg19a  30797  cdlemg19  30798  cdlemg28a  30807  cdlemg27b  30810  cdlemg28b  30817  cdlemg28  30818  cdlemg33a  30820  cdlemg33b  30821  cdlemg33c  30822  cdlemg33d  30823  cdlemg33e  30824  cdlemg33  30825  cdlemg35  30827  cdlemg36  30828  cdlemg44a  30845  cdlemh  30931  cdlemi2  30933  cdlemj1  30935  tendocan  30938  cdlemk5a  30949  cdlemki  30955  cdlemkvcl  30956  cdlemk10  30957  cdlemksv2  30961  cdlemkole  30967  cdlemk14  30968  cdlemk15  30969  cdlemk16a  30970  cdlemk16  30971  cdlemk17  30972  cdlemk18  30982  cdlemk19  30983  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  cdlemk30  31008  cdlemk18-3N  31014  cdlemk23-3  31016  cdlemk25-3  31018  cdlemk27-3  31021  cdlemk37  31028  cdlemkfid1N  31035  cdlemkid1  31036  cdlemky  31040  cdlemk11ta  31043  cdlemk47  31063  cdlemk48  31064  cdlemk49  31065  cdlemk50  31066  cdlemk51  31067  cdlemk52  31068  cdlemk53a  31069  cdlemk54  31072  cdlemk39u1  31081  cdlemk19u1  31083  cdleml1N  31090  cdleml2N  31091  cdleml3N  31092  dia2dimlem6  31184  cdlemn2  31310  cdlemn2a  31311  cdlemn5pre  31315  cdlemn10  31321  cdlemn11c  31324  cdlemn11pre  31325  dihjustlem  31331  dihjust  31332  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