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

Theorem simp21l 1105
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 1012 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  modexp  12102  segconeu  28178  4atlem10  33558  lplncvrlvol2  33567  4atex  34028  4atex2-0cOLDN  34032  cdlemd2  34151  cdlemd3  34152  cdlemd4  34153  cdleme0e  34169  cdleme0moN  34177  cdleme3g  34186  cdleme3h  34187  cdleme3  34189  cdleme9  34205  cdleme11c  34213  cdleme11dN  34214  cdleme11e  34215  cdleme11fN  34216  cdleme11h  34218  cdleme11j  34219  cdleme11k  34220  cdleme11  34222  cdleme12  34223  cdleme13  34224  cdleme14  34225  cdleme15a  34226  cdleme15b  34227  cdleme15c  34228  cdleme15d  34229  cdleme15  34230  cdleme16b  34231  cdleme16c  34232  cdleme16d  34233  cdleme16e  34234  cdleme16f  34235  cdleme17d1  34241  cdleme18a  34243  cdleme18b  34244  cdleme18c  34245  cdleme18d  34247  cdleme19b  34256  cdleme19d  34258  cdleme19e  34259  cdleme20c  34263  cdleme20d  34264  cdleme20e  34265  cdleme20f  34266  cdleme20g  34267  cdleme20h  34268  cdleme20j  34270  cdleme20l2  34273  cdleme20l  34274  cdleme20m  34275  cdleme20  34276  cdleme21ct  34281  cdleme21e  34283  cdleme21i  34287  cdleme22aa  34291  cdleme22cN  34294  cdleme22d  34295  cdleme22e  34296  cdleme22eALTN  34297  cdleme22f  34298  cdleme26e  34311  cdleme27a  34319  cdleme32e  34397  cdlemg2fv2  34552  cdlemg4a  34560  cdlemg4d  34565  cdlemg4  34569  cdlemg6c  34572  cdlemg8b  34580  cdlemg8c  34581  cdlemg9a  34584  cdlemg9  34586  cdlemg12a  34595  cdlemg12c  34597  cdlemg17dALTN  34616  cdlemg17h  34620  cdlemg18b  34631  cdlemg18c  34632  cdlemg18d  34633  cdlemg18  34634  cdlemg19a  34635  cdlemg21  34638  cdlemg28a  34645  cdlemg31b0a  34647  cdlemg31d  34652  cdlemg33b0  34653  cdlemg33a  34658  cdlemh  34769  cdlemk5  34788  cdlemk6  34789  cdlemk7  34800  cdlemk11  34801  cdlemk12  34802  cdlemk21N  34825  cdlemk20  34826  cdlemk28-3  34860  cdlemk34  34862  cdlemkfid3N  34877  cdlemk35s-id  34890  cdlemk39s-id  34892  cdlemk55u1  34917  cdlemn2  35148  cdlemn10  35159  dihjustlem  35169
  Copyright terms: Public domain W3C validator