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

Theorem simp21l 1072
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 979 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 977 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  modexp  11236  segconeu  24634  4atlem10  29795  lplncvrlvol2  29804  4atex  30265  4atex2-0cOLDN  30269  cdlemd2  30388  cdlemd3  30389  cdlemd4  30390  cdleme0e  30406  cdleme0moN  30414  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme9  30442  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11fN  30453  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme11  30459  cdleme12  30460  cdleme13  30461  cdleme14  30462  cdleme15a  30463  cdleme15b  30464  cdleme15c  30465  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17d1  30478  cdleme18a  30480  cdleme18b  30481  cdleme18c  30482  cdleme18d  30484  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20c  30500  cdleme20d  30501  cdleme20e  30502  cdleme20f  30503  cdleme20g  30504  cdleme20h  30505  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme20  30513  cdleme21ct  30518  cdleme21e  30520  cdleme21i  30524  cdleme22aa  30528  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme26e  30548  cdleme27a  30556  cdleme32e  30634  cdlemg2fv2  30789  cdlemg4a  30797  cdlemg4d  30802  cdlemg4  30806  cdlemg6c  30809  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9  30823  cdlemg12a  30832  cdlemg12c  30834  cdlemg17dALTN  30853  cdlemg17h  30857  cdlemg18b  30868  cdlemg18c  30869  cdlemg18d  30870  cdlemg18  30871  cdlemg19a  30872  cdlemg21  30875  cdlemg28a  30882  cdlemg31b0a  30884  cdlemg31d  30889  cdlemg33b0  30890  cdlemg33a  30895  cdlemh  31006  cdlemk5  31025  cdlemk6  31026  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemk21N  31062  cdlemk20  31063  cdlemk28-3  31097  cdlemk34  31099  cdlemkfid3N  31114  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk55u1  31154  cdlemn2  31385  cdlemn10  31396  dihjustlem  31406
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