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  6582  cofsmo  7897  axdc4lem  8083  0catg  13591  funcoppc  13751  funcres  13772  catcisolem  13940  1stfcl  13973  2ndfcl  13974  prfcl  13979  evlfcl  13998  curf1cl  14004  curfcl  14008  hofcl  14035  meetle  14136  mulgdirlem  14593  prdsxmetlem  17934  isosctrlem3  20122  isosctr  20123  amgmlem  20286  colinearalg  24540  ax5seglem6  24564  ax5seg  24568  axpasch  24571  axeuclidlem  24592  axeuclid  24593  cgrtr  24617  cgrtr3  24619  ofscom  24632  segconeq  24635  ifscgr  24669  btwnxfr  24681  colinearxfr  24700  lineext  24701  brofs2  24702  brifs2  24703  fscgr  24705  linecgr  24706  btwnconn1lem1  24712  btwnconn1lem2  24713  btwnconn1lem3  24714  btwnconn1lem4  24715  btwnconn1lem5  24716  btwnconn1lem6  24717  btwnconn1lem7  24718  seglecgr12im  24735  seglecgr12  24736  segletr  24739  broutsideof3  24751  outsideofeq  24755  lineunray  24772  lineelsb2  24773  linecom  24775  cmpmorass  25977  bisig0  26073  isig1a2  26074  bnj1128  29093  lshpkrlem5  29377  omlmod1i2N  29523  cvrnbtwn3  29539  cvrcmp  29546  cvrcmp2  29547  cvlexch2  29592  cvlexchb2  29594  cvlatexchb2  29598  cvlatexch2  29600  cvlatexch3  29601  cvlsupr7  29611  atnlej1  29641  atnlej2  29642  2llnneN  29671  cvratlem  29683  atcvrneN  29692  atcvrj1  29693  atlelt  29700  2atjm  29707  3noncolr2  29711  3noncolr1N  29712  3dimlem2  29721  3dim1  29729  3dim2  29730  1cvrat  29738  ps-1  29739  ps-2  29740  2atjlej  29741  hlatexch3N  29742  ps-2b  29744  3atlem1  29745  3atlem2  29746  3atlem5  29749  3atlem6  29750  llnle  29780  2atm  29789  ps-2c  29790  lplni2  29799  lplnle  29802  lplnnle2at  29803  lplnri3N  29817  llncvrlpln2  29819  2atmat  29823  2llnm2N  29830  2llnm4  29832  2llnmeqat  29833  lvolnle3at  29844  4atlem0ae  29856  4atlem0be  29857  4atlem3b  29860  4atlem9  29865  4atlem10a  29866  4atlem10  29868  4atlem11a  29869  4atlem12a  29872  4at2  29876  2lplnm2N  29883  lneq2at  30040  2llnma1b  30048  2llnma1  30049  2llnma3r  30050  2llnma2  30051  2llnma2rN  30052  cdlema1N  30053  paddasslem2  30083  paddasslem15  30096  paddasslem16  30097  pmodlem1  30108  pmodlem2  30109  pmod2iN  30111  hlmod1i  30118  atmod1i1m  30120  atmod2i1  30123  atmod2i2  30124  atmod3i1  30126  atmod3i2  30127  atmod4i1  30128  atmod4i2  30129  llnexchb2lem  30130  llnexch2N  30132  dalawlem3  30135  dalawlem4  30136  dalawlem5  30137  dalawlem6  30138  dalawlem7  30139  dalawlem8  30140  dalawlem9  30141  dalawlem11  30143  dalawlem12  30144  dalawlem13  30145  dalawlem15  30147  osumcllem9N  30226  pl42lem1N  30241  4atexlems  30314  4atex2  30339  4atex2-0bOLDN  30341  trlval4  30450  cdlemc5  30457  cdlemc6  30458  cdlemd2  30461  cdlemd4  30463  cdlemd6  30465  cdleme00a  30471  cdleme0e  30479  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4  30500  cdleme4a  30501  cdleme5  30502  cdleme9  30515  cdleme16aN  30521  cdleme11c  30523  cdleme11e  30525  cdleme11g  30527  cdleme11h  30528  cdleme11j  30529  cdleme11k  30530  cdleme11l  30531  cdleme11  30532  cdleme12  30533  cdleme14  30535  cdleme15c  30538  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme0nex  30552  cdleme18a  30553  cdleme18c  30555  cdleme18d  30557  cdlemednpq  30561  cdlemednuN  30562  cdleme20zN  30563  cdleme20y  30564  cdleme19a  30565  cdleme19b  30566  cdleme19d  30568  cdleme19e  30569  cdleme20aN  30571  cdleme20bN  30572  cdleme20c  30573  cdleme20d  30574  cdleme20f  30576  cdleme20g  30577  cdleme20i  30579  cdleme20j  30580  cdleme20l1  30582  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21b  30588  cdleme21c  30589  cdleme21e  30593  cdleme21f  30594  cdleme22a  30602  cdleme22b  30603  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f  30608  cdleme26eALTN  30623  cdleme26fALTN  30624  cdleme26f  30625  cdleme26f2ALTN  30626  cdleme26f2  30627  cdleme27N  30631  cdleme28a  30632  cdleme28b  30633  cdleme30a  30640  cdleme43fsv1snlem  30682  cdlemefs31fv1  30686  cdlemefs45eN  30693  cdleme32b  30704  cdleme32c  30705  cdleme32d  30706  cdleme35h  30718  cdleme36a  30722  cdleme36m  30723  cdleme37m  30724  cdleme40m  30729  cdleme40n  30730  cdleme41sn3aw  30736  cdleme41sn4aw  30737  cdleme41fva11  30739  cdleme42k  30746  cdleme43cN  30753  cdleme43dN  30754  cdleme46f2g1  30756  cdlemeg47rv2  30772  cdlemeg46sfg  30782  cdlemeg46fjgN  30783  cdlemeg46rjgN  30784  cdlemeg46fjv  30785  cdlemeg46frv  30787  cdlemeg46vrg  30789  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfv  30792  cdlemg4a  30870  cdlemg4d  30875  cdlemg4e  30876  cdlemg4f  30877  cdlemg4g  30878  cdlemg4  30879  cdlemg6d  30883  cdlemg6e  30884  cdlemg8b  30890  cdlemg8c  30891  cdlemg9a  30894  cdlemg9b  30895  cdlemg10a  30902  cdlemg10  30903  cdlemg12a  30905  cdlemg12b  30906  cdlemg12f  30910  cdlemg12g  30911  cdlemg12  30912  cdlemg17dN  30925  cdlemg17dALTN  30926  cdlemg17e  30927  cdlemg17f  30928  cdlemg17g  30929  cdlemg17h  30930  cdlemg17i  30931  cdlemg17pq  30934  cdlemg17iqN  30936  cdlemg17  30939  cdlemg18b  30941  cdlemg18c  30942  cdlemg19a  30945  cdlemg19  30946  cdlemg28a  30955  cdlemg27b  30958  cdlemg28b  30965  cdlemg28  30966  cdlemg33a  30968  cdlemg33b  30969  cdlemg33c  30970  cdlemg33d  30971  cdlemg33e  30972  cdlemg33  30973  cdlemg35  30975  cdlemg36  30976  cdlemg44a  30993  cdlemh  31079  cdlemi2  31081  cdlemj1  31083  tendocan  31086  cdlemk5a  31097  cdlemki  31103  cdlemkvcl  31104  cdlemk10  31105  cdlemksv2  31109  cdlemkole  31115  cdlemk14  31116  cdlemk15  31117  cdlemk16a  31118  cdlemk16  31119  cdlemk17  31120  cdlemk18  31130  cdlemk19  31131  cdlemkoatnle-2N  31137  cdlemk13-2N  31138  cdlemkole-2N  31139  cdlemk14-2N  31140  cdlemk15-2N  31141  cdlemk16-2N  31142  cdlemk17-2N  31143  cdlemk18-2N  31148  cdlemk19-2N  31149  cdlemk30  31156  cdlemk18-3N  31162  cdlemk23-3  31164  cdlemk25-3  31166  cdlemk27-3  31169  cdlemk37  31176  cdlemkfid1N  31183  cdlemkid1  31184  cdlemky  31188  cdlemk11ta  31191  cdlemk47  31211  cdlemk48  31212  cdlemk49  31213  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk53a  31217  cdlemk54  31220  cdlemk39u1  31229  cdlemk19u1  31231  cdleml1N  31238  cdleml2N  31239  cdleml3N  31240  dia2dimlem6  31332  cdlemn2  31458  cdlemn2a  31459  cdlemn5pre  31463  cdlemn10  31469  cdlemn11c  31472  cdlemn11pre  31473  dihjustlem  31479  dihjust  31480  lclkrlem2y  31794
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