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  6816  cofsmo  8138  axdc4lem  8324  0catg  13900  funcoppc  14060  funcres  14081  catcisolem  14249  1stfcl  14282  2ndfcl  14283  prfcl  14288  evlfcl  14307  curf1cl  14313  curfcl  14317  hofcl  14344  meetle  14445  mulgdirlem  14902  prdsxmetlem  18386  isosctrlem3  20652  isosctr  20653  amgmlem  20816  ofldaddlt  24229  rhmdvd  24247  colinearalg  25797  ax5seglem6  25821  ax5seg  25825  axpasch  25828  axeuclidlem  25849  axeuclid  25850  cgrtr  25874  cgrtr3  25876  ofscom  25889  segconeq  25892  ifscgr  25926  btwnxfr  25938  colinearxfr  25957  lineext  25958  brofs2  25959  brifs2  25960  fscgr  25962  linecgr  25963  btwnconn1lem1  25969  btwnconn1lem2  25970  btwnconn1lem3  25971  btwnconn1lem4  25972  btwnconn1lem5  25973  btwnconn1lem6  25974  btwnconn1lem7  25975  seglecgr12im  25992  seglecgr12  25993  segletr  25996  broutsideof3  26008  outsideofeq  26012  lineunray  26029  lineelsb2  26030  linecom  26032  bnj1128  29213  lshpkrlem5  29751  omlmod1i2N  29897  cvrnbtwn3  29913  cvrcmp  29920  cvrcmp2  29921  cvlexch2  29966  cvlexchb2  29968  cvlatexchb2  29972  cvlatexch2  29974  cvlatexch3  29975  cvlsupr7  29985  atnlej1  30015  atnlej2  30016  2llnneN  30045  cvratlem  30057  atcvrneN  30066  atcvrj1  30067  atlelt  30074  2atjm  30081  3noncolr2  30085  3noncolr1N  30086  3dimlem2  30095  3dim1  30103  3dim2  30104  1cvrat  30112  ps-1  30113  ps-2  30114  2atjlej  30115  hlatexch3N  30116  ps-2b  30118  3atlem1  30119  3atlem2  30120  3atlem5  30123  3atlem6  30124  llnle  30154  2atm  30163  ps-2c  30164  lplni2  30173  lplnle  30176  lplnnle2at  30177  lplnri3N  30191  llncvrlpln2  30193  2atmat  30197  2llnm2N  30204  2llnm4  30206  2llnmeqat  30207  lvolnle3at  30218  4atlem0ae  30230  4atlem0be  30231  4atlem3b  30234  4atlem9  30239  4atlem10a  30240  4atlem10  30242  4atlem11a  30243  4atlem12a  30246  4at2  30250  2lplnm2N  30257  lneq2at  30414  2llnma1b  30422  2llnma1  30423  2llnma3r  30424  2llnma2  30425  2llnma2rN  30426  cdlema1N  30427  paddasslem2  30457  paddasslem15  30470  paddasslem16  30471  pmodlem1  30482  pmodlem2  30483  pmod2iN  30485  hlmod1i  30492  atmod1i1m  30494  atmod2i1  30497  atmod2i2  30498  atmod3i1  30500  atmod3i2  30501  atmod4i1  30502  atmod4i2  30503  llnexchb2lem  30504  llnexch2N  30506  dalawlem3  30509  dalawlem4  30510  dalawlem5  30511  dalawlem6  30512  dalawlem7  30513  dalawlem8  30514  dalawlem9  30515  dalawlem11  30517  dalawlem12  30518  dalawlem13  30519  dalawlem15  30521  osumcllem9N  30600  pl42lem1N  30615  4atexlems  30688  4atex2  30713  4atex2-0bOLDN  30715  trlval4  30824  cdlemc5  30831  cdlemc6  30832  cdlemd2  30835  cdlemd4  30837  cdlemd6  30839  cdleme00a  30845  cdleme0e  30853  cdleme3g  30870  cdleme3h  30871  cdleme3  30873  cdleme4  30874  cdleme4a  30875  cdleme5  30876  cdleme9  30889  cdleme16aN  30895  cdleme11c  30897  cdleme11e  30899  cdleme11g  30901  cdleme11h  30902  cdleme11j  30903  cdleme11k  30904  cdleme11l  30905  cdleme11  30906  cdleme12  30907  cdleme14  30909  cdleme15c  30912  cdleme16b  30915  cdleme16c  30916  cdleme16d  30917  cdleme16e  30918  cdleme16f  30919  cdleme0nex  30926  cdleme18a  30927  cdleme18c  30929  cdleme18d  30931  cdlemednpq  30935  cdlemednuN  30936  cdleme20zN  30937  cdleme20y  30938  cdleme19a  30939  cdleme19b  30940  cdleme19d  30942  cdleme19e  30943  cdleme20aN  30945  cdleme20bN  30946  cdleme20c  30947  cdleme20d  30948  cdleme20f  30950  cdleme20g  30951  cdleme20i  30953  cdleme20j  30954  cdleme20l1  30956  cdleme20l2  30957  cdleme20l  30958  cdleme20m  30959  cdleme21b  30962  cdleme21c  30963  cdleme21e  30967  cdleme21f  30968  cdleme22a  30976  cdleme22b  30977  cdleme22e  30980  cdleme22eALTN  30981  cdleme22f  30982  cdleme26eALTN  30997  cdleme26fALTN  30998  cdleme26f  30999  cdleme26f2ALTN  31000  cdleme26f2  31001  cdleme27N  31005  cdleme28a  31006  cdleme28b  31007  cdleme30a  31014  cdleme43fsv1snlem  31056  cdlemefs31fv1  31060  cdlemefs45eN  31067  cdleme32b  31078  cdleme32c  31079  cdleme32d  31080  cdleme35h  31092  cdleme36a  31096  cdleme36m  31097  cdleme37m  31098  cdleme40m  31103  cdleme40n  31104  cdleme41sn3aw  31110  cdleme41sn4aw  31111  cdleme41fva11  31113  cdleme42k  31120  cdleme43cN  31127  cdleme43dN  31128  cdleme46f2g1  31130  cdlemeg47rv2  31146  cdlemeg46sfg  31156  cdlemeg46fjgN  31157  cdlemeg46rjgN  31158  cdlemeg46fjv  31159  cdlemeg46frv  31161  cdlemeg46vrg  31163  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemeg46gfv  31166  cdlemg4a  31244  cdlemg4d  31249  cdlemg4e  31250  cdlemg4f  31251  cdlemg4g  31252  cdlemg4  31253  cdlemg6d  31257  cdlemg6e  31258  cdlemg8b  31264  cdlemg8c  31265  cdlemg9a  31268  cdlemg9b  31269  cdlemg10a  31276  cdlemg10  31277  cdlemg12a  31279  cdlemg12b  31280  cdlemg12f  31284  cdlemg12g  31285  cdlemg12  31286  cdlemg17dN  31299  cdlemg17dALTN  31300  cdlemg17e  31301  cdlemg17f  31302  cdlemg17g  31303  cdlemg17h  31304  cdlemg17i  31305  cdlemg17pq  31308  cdlemg17iqN  31310  cdlemg17  31313  cdlemg18b  31315  cdlemg18c  31316  cdlemg19a  31319  cdlemg19  31320  cdlemg28a  31329  cdlemg27b  31332  cdlemg28b  31339  cdlemg28  31340  cdlemg33a  31342  cdlemg33b  31343  cdlemg33c  31344  cdlemg33d  31345  cdlemg33e  31346  cdlemg33  31347  cdlemg35  31349  cdlemg36  31350  cdlemg44a  31367  cdlemh  31453  cdlemi2  31455  cdlemj1  31457  tendocan  31460  cdlemk5a  31471  cdlemki  31477  cdlemkvcl  31478  cdlemk10  31479  cdlemksv2  31483  cdlemkole  31489  cdlemk14  31490  cdlemk15  31491  cdlemk16a  31492  cdlemk16  31493  cdlemk17  31494  cdlemk18  31504  cdlemk19  31505  cdlemkoatnle-2N  31511  cdlemk13-2N  31512  cdlemkole-2N  31513  cdlemk14-2N  31514  cdlemk15-2N  31515  cdlemk16-2N  31516  cdlemk17-2N  31517  cdlemk18-2N  31522  cdlemk19-2N  31523  cdlemk30  31530  cdlemk18-3N  31536  cdlemk23-3  31538  cdlemk25-3  31540  cdlemk27-3  31543  cdlemk37  31550  cdlemkfid1N  31557  cdlemkid1  31558  cdlemky  31562  cdlemk11ta  31565  cdlemk47  31585  cdlemk48  31586  cdlemk49  31587  cdlemk50  31588  cdlemk51  31589  cdlemk52  31590  cdlemk53a  31591  cdlemk54  31594  cdlemk39u1  31603  cdlemk19u1  31605  cdleml1N  31612  cdleml2N  31613  cdleml3N  31614  dia2dimlem6  31706  cdlemn2  31832  cdlemn2a  31833  cdlemn5pre  31837  cdlemn10  31843  cdlemn11c  31846  cdlemn11pre  31847  dihjustlem  31853  dihjust  31854  lclkrlem2y  32168
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