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  6580  cofsmo  7895  axdc4lem  8081  0catg  13589  funcoppc  13749  funcres  13770  catcisolem  13938  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  meetle  14134  mulgdirlem  14591  prdsxmetlem  17932  isosctrlem3  20120  isosctr  20121  amgmlem  20284  colinearalg  24538  ax5seglem6  24562  ax5seg  24566  axpasch  24569  axeuclidlem  24590  axeuclid  24591  cgrtr  24615  cgrtr3  24617  ofscom  24630  segconeq  24633  ifscgr  24667  btwnxfr  24679  colinearxfr  24698  lineext  24699  brofs2  24700  brifs2  24701  fscgr  24703  linecgr  24704  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  seglecgr12im  24733  seglecgr12  24734  segletr  24737  broutsideof3  24749  outsideofeq  24753  lineunray  24770  lineelsb2  24771  linecom  24773  cmpmorass  25966  bisig0  26062  isig1a2  26063  bnj1128  29020  lshpkrlem5  29304  omlmod1i2N  29450  cvrnbtwn3  29466  cvrcmp  29473  cvrcmp2  29474  cvlexch2  29519  cvlexchb2  29521  cvlatexchb2  29525  cvlatexch2  29527  cvlatexch3  29528  cvlsupr7  29538  atnlej1  29568  atnlej2  29569  2llnneN  29598  cvratlem  29610  atcvrneN  29619  atcvrj1  29620  atlelt  29627  2atjm  29634  3noncolr2  29638  3noncolr1N  29639  3dimlem2  29648  3dim1  29656  3dim2  29657  1cvrat  29665  ps-1  29666  ps-2  29667  2atjlej  29668  hlatexch3N  29669  ps-2b  29671  3atlem1  29672  3atlem2  29673  3atlem5  29676  3atlem6  29677  llnle  29707  2atm  29716  ps-2c  29717  lplni2  29726  lplnle  29729  lplnnle2at  29730  lplnri3N  29744  llncvrlpln2  29746  2atmat  29750  2llnm2N  29757  2llnm4  29759  2llnmeqat  29760  lvolnle3at  29771  4atlem0ae  29783  4atlem0be  29784  4atlem3b  29787  4atlem9  29792  4atlem10a  29793  4atlem10  29795  4atlem11a  29796  4atlem12a  29799  4at2  29803  2lplnm2N  29810  lneq2at  29967  2llnma1b  29975  2llnma1  29976  2llnma3r  29977  2llnma2  29978  2llnma2rN  29979  cdlema1N  29980  paddasslem2  30010  paddasslem15  30023  paddasslem16  30024  pmodlem1  30035  pmodlem2  30036  pmod2iN  30038  hlmod1i  30045  atmod1i1m  30047  atmod2i1  30050  atmod2i2  30051  atmod3i1  30053  atmod3i2  30054  atmod4i1  30055  atmod4i2  30056  llnexchb2lem  30057  llnexch2N  30059  dalawlem3  30062  dalawlem4  30063  dalawlem5  30064  dalawlem6  30065  dalawlem7  30066  dalawlem8  30067  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  dalawlem13  30072  dalawlem15  30074  osumcllem9N  30153  pl42lem1N  30168  4atexlems  30241  4atex2  30266  4atex2-0bOLDN  30268  trlval4  30377  cdlemc5  30384  cdlemc6  30385  cdlemd2  30388  cdlemd4  30390  cdlemd6  30392  cdleme00a  30398  cdleme0e  30406  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme4  30427  cdleme4a  30428  cdleme5  30429  cdleme9  30442  cdleme16aN  30448  cdleme11c  30450  cdleme11e  30452  cdleme11g  30454  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme11l  30458  cdleme11  30459  cdleme12  30460  cdleme14  30462  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme0nex  30479  cdleme18a  30480  cdleme18c  30482  cdleme18d  30484  cdlemednpq  30488  cdlemednuN  30489  cdleme20zN  30490  cdleme20y  30491  cdleme19a  30492  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20aN  30498  cdleme20bN  30499  cdleme20c  30500  cdleme20d  30501  cdleme20f  30503  cdleme20g  30504  cdleme20i  30506  cdleme20j  30507  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21b  30515  cdleme21c  30516  cdleme21e  30520  cdleme21f  30521  cdleme22a  30529  cdleme22b  30530  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme26eALTN  30550  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme30a  30567  cdleme43fsv1snlem  30609  cdlemefs31fv1  30613  cdlemefs45eN  30620  cdleme32b  30631  cdleme32c  30632  cdleme32d  30633  cdleme35h  30645  cdleme36a  30649  cdleme36m  30650  cdleme37m  30651  cdleme40m  30656  cdleme40n  30657  cdleme41sn3aw  30663  cdleme41sn4aw  30664  cdleme41fva11  30666  cdleme42k  30673  cdleme43cN  30680  cdleme43dN  30681  cdleme46f2g1  30683  cdlemeg47rv2  30699  cdlemeg46sfg  30709  cdlemeg46fjgN  30710  cdlemeg46rjgN  30711  cdlemeg46fjv  30712  cdlemeg46frv  30714  cdlemeg46vrg  30716  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdlemg4a  30797  cdlemg4d  30802  cdlemg4e  30803  cdlemg4f  30804  cdlemg4g  30805  cdlemg4  30806  cdlemg6d  30810  cdlemg6e  30811  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg10a  30829  cdlemg10  30830  cdlemg12a  30832  cdlemg12b  30833  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg17dN  30852  cdlemg17dALTN  30853  cdlemg17e  30854  cdlemg17f  30855  cdlemg17g  30856  cdlemg17h  30857  cdlemg17i  30858  cdlemg17pq  30861  cdlemg17iqN  30863  cdlemg17  30866  cdlemg18b  30868  cdlemg18c  30869  cdlemg19a  30872  cdlemg19  30873  cdlemg28a  30882  cdlemg27b  30885  cdlemg28b  30892  cdlemg28  30893  cdlemg33a  30895  cdlemg33b  30896  cdlemg33c  30897  cdlemg33d  30898  cdlemg33e  30899  cdlemg33  30900  cdlemg35  30902  cdlemg36  30903  cdlemg44a  30920  cdlemh  31006  cdlemi2  31008  cdlemj1  31010  tendocan  31013  cdlemk5a  31024  cdlemki  31030  cdlemkvcl  31031  cdlemk10  31032  cdlemksv2  31036  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk16a  31045  cdlemk16  31046  cdlemk17  31047  cdlemk18  31057  cdlemk19  31058  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk30  31083  cdlemk18-3N  31089  cdlemk23-3  31091  cdlemk25-3  31093  cdlemk27-3  31096  cdlemk37  31103  cdlemkfid1N  31110  cdlemkid1  31111  cdlemky  31115  cdlemk11ta  31118  cdlemk47  31138  cdlemk48  31139  cdlemk49  31140  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk54  31147  cdlemk39u1  31156  cdlemk19u1  31158  cdleml1N  31165  cdleml2N  31166  cdleml3N  31167  dia2dimlem6  31259  cdlemn2  31385  cdlemn2a  31386  cdlemn5pre  31390  cdlemn10  31396  cdlemn11c  31399  cdlemn11pre  31400  dihjustlem  31406  dihjust  31407  lclkrlem2y  31721
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