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

Theorem simp21l 1075
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 980 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  modexp  11516  segconeu  25947  4atlem10  30465  lplncvrlvol2  30474  4atex  30935  4atex2-0cOLDN  30939  cdlemd2  31058  cdlemd3  31059  cdlemd4  31060  cdleme0e  31076  cdleme0moN  31084  cdleme3g  31093  cdleme3h  31094  cdleme3  31096  cdleme9  31112  cdleme11c  31120  cdleme11dN  31121  cdleme11e  31122  cdleme11fN  31123  cdleme11h  31125  cdleme11j  31126  cdleme11k  31127  cdleme11  31129  cdleme12  31130  cdleme13  31131  cdleme14  31132  cdleme15a  31133  cdleme15b  31134  cdleme15c  31135  cdleme15d  31136  cdleme15  31137  cdleme16b  31138  cdleme16c  31139  cdleme16d  31140  cdleme16e  31141  cdleme16f  31142  cdleme17d1  31148  cdleme18a  31150  cdleme18b  31151  cdleme18c  31152  cdleme18d  31154  cdleme19b  31163  cdleme19d  31165  cdleme19e  31166  cdleme20c  31170  cdleme20d  31171  cdleme20e  31172  cdleme20f  31173  cdleme20g  31174  cdleme20h  31175  cdleme20j  31177  cdleme20l2  31180  cdleme20l  31181  cdleme20m  31182  cdleme20  31183  cdleme21ct  31188  cdleme21e  31190  cdleme21i  31194  cdleme22aa  31198  cdleme22cN  31201  cdleme22d  31202  cdleme22e  31203  cdleme22eALTN  31204  cdleme22f  31205  cdleme26e  31218  cdleme27a  31226  cdleme32e  31304  cdlemg2fv2  31459  cdlemg4a  31467  cdlemg4d  31472  cdlemg4  31476  cdlemg6c  31479  cdlemg8b  31487  cdlemg8c  31488  cdlemg9a  31491  cdlemg9  31493  cdlemg12a  31502  cdlemg12c  31504  cdlemg17dALTN  31523  cdlemg17h  31527  cdlemg18b  31538  cdlemg18c  31539  cdlemg18d  31540  cdlemg18  31541  cdlemg19a  31542  cdlemg21  31545  cdlemg28a  31552  cdlemg31b0a  31554  cdlemg31d  31559  cdlemg33b0  31560  cdlemg33a  31565  cdlemh  31676  cdlemk5  31695  cdlemk6  31696  cdlemk7  31707  cdlemk11  31708  cdlemk12  31709  cdlemk21N  31732  cdlemk20  31733  cdlemk28-3  31767  cdlemk34  31769  cdlemkfid3N  31784  cdlemk35s-id  31797  cdlemk39s-id  31799  cdlemk55u1  31824  cdlemn2  32055  cdlemn10  32066  dihjustlem  32076
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator