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

Theorem simp21l 1122
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21l  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1029 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 1027 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  modexp  12404  segconeu  30563  4atlem10  32880  lplncvrlvol2  32889  4atex  33350  4atex2-0cOLDN  33354  cdlemd2  33474  cdlemd3  33475  cdlemd4  33476  cdleme0e  33492  cdleme0moN  33500  cdleme3g  33509  cdleme3h  33510  cdleme3  33512  cdleme9  33528  cdleme11c  33536  cdleme11dN  33537  cdleme11e  33538  cdleme11fN  33539  cdleme11h  33541  cdleme11j  33542  cdleme11k  33543  cdleme11  33545  cdleme12  33546  cdleme13  33547  cdleme14  33548  cdleme15a  33549  cdleme15b  33550  cdleme15c  33551  cdleme15d  33552  cdleme15  33553  cdleme16b  33554  cdleme16c  33555  cdleme16d  33556  cdleme16e  33557  cdleme16f  33558  cdleme17d1  33564  cdleme18a  33566  cdleme18b  33567  cdleme18c  33568  cdleme18d  33570  cdleme19b  33580  cdleme19d  33582  cdleme19e  33583  cdleme20c  33587  cdleme20d  33588  cdleme20e  33589  cdleme20f  33590  cdleme20g  33591  cdleme20h  33592  cdleme20j  33594  cdleme20l2  33597  cdleme20l  33598  cdleme20m  33599  cdleme20  33600  cdleme21ct  33605  cdleme21e  33607  cdleme21i  33611  cdleme22aa  33615  cdleme22cN  33618  cdleme22d  33619  cdleme22e  33620  cdleme22eALTN  33621  cdleme22f  33622  cdleme26e  33635  cdleme27a  33643  cdleme32e  33721  cdlemg2fv2  33876  cdlemg4a  33884  cdlemg4d  33889  cdlemg4  33893  cdlemg6c  33896  cdlemg8b  33904  cdlemg8c  33905  cdlemg9a  33908  cdlemg9  33910  cdlemg12a  33919  cdlemg12c  33921  cdlemg17dALTN  33940  cdlemg17h  33944  cdlemg18b  33955  cdlemg18c  33956  cdlemg18d  33957  cdlemg18  33958  cdlemg19a  33959  cdlemg21  33962  cdlemg28a  33969  cdlemg31b0a  33971  cdlemg31d  33976  cdlemg33b0  33977  cdlemg33a  33982  cdlemh  34093  cdlemk5  34112  cdlemk6  34113  cdlemk7  34124  cdlemk11  34125  cdlemk12  34126  cdlemk21N  34149  cdlemk20  34150  cdlemk28-3  34184  cdlemk34  34186  cdlemkfid3N  34201  cdlemk35s-id  34214  cdlemk39s-id  34216  cdlemk55u1  34241  cdlemn2  34472  cdlemn10  34483  dihjustlem  34493
  Copyright terms: Public domain W3C validator