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  11252  segconeu  24706  4atlem10  30417  lplncvrlvol2  30426  4atex  30887  4atex2-0cOLDN  30891  cdlemd2  31010  cdlemd3  31011  cdlemd4  31012  cdleme0e  31028  cdleme0moN  31036  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme9  31064  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11fN  31075  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme11  31081  cdleme12  31082  cdleme13  31083  cdleme14  31084  cdleme15a  31085  cdleme15b  31086  cdleme15c  31087  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17d1  31100  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme18d  31106  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20c  31122  cdleme20d  31123  cdleme20e  31124  cdleme20f  31125  cdleme20g  31126  cdleme20h  31127  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme20  31135  cdleme21ct  31140  cdleme21e  31142  cdleme21i  31146  cdleme22aa  31150  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme26e  31170  cdleme27a  31178  cdleme32e  31256  cdlemg2fv2  31411  cdlemg4a  31419  cdlemg4d  31424  cdlemg4  31428  cdlemg6c  31431  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9  31445  cdlemg12a  31454  cdlemg12c  31456  cdlemg17dALTN  31475  cdlemg17h  31479  cdlemg18b  31490  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg19a  31494  cdlemg21  31497  cdlemg28a  31504  cdlemg31b0a  31506  cdlemg31d  31511  cdlemg33b0  31512  cdlemg33a  31517  cdlemh  31628  cdlemk5  31647  cdlemk6  31648  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemk21N  31684  cdlemk20  31685  cdlemk28-3  31719  cdlemk34  31721  cdlemkfid3N  31736  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk55u1  31776  cdlemn2  32007  cdlemn10  32018  dihjustlem  32028
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