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

Theorem simp21l 1074
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 979 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  modexp  11469  segconeu  25849  4atlem10  30088  lplncvrlvol2  30097  4atex  30558  4atex2-0cOLDN  30562  cdlemd2  30681  cdlemd3  30682  cdlemd4  30683  cdleme0e  30699  cdleme0moN  30707  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme9  30735  cdleme11c  30743  cdleme11dN  30744  cdleme11e  30745  cdleme11fN  30746  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme11  30752  cdleme12  30753  cdleme13  30754  cdleme14  30755  cdleme15a  30756  cdleme15b  30757  cdleme15c  30758  cdleme15d  30759  cdleme15  30760  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17d1  30771  cdleme18a  30773  cdleme18b  30774  cdleme18c  30775  cdleme18d  30777  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20c  30793  cdleme20d  30794  cdleme20e  30795  cdleme20f  30796  cdleme20g  30797  cdleme20h  30798  cdleme20j  30800  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme20  30806  cdleme21ct  30811  cdleme21e  30813  cdleme21i  30817  cdleme22aa  30821  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme26e  30841  cdleme27a  30849  cdleme32e  30927  cdlemg2fv2  31082  cdlemg4a  31090  cdlemg4d  31095  cdlemg4  31099  cdlemg6c  31102  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg9  31116  cdlemg12a  31125  cdlemg12c  31127  cdlemg17dALTN  31146  cdlemg17h  31150  cdlemg18b  31161  cdlemg18c  31162  cdlemg18d  31163  cdlemg18  31164  cdlemg19a  31165  cdlemg21  31168  cdlemg28a  31175  cdlemg31b0a  31177  cdlemg31d  31182  cdlemg33b0  31183  cdlemg33a  31188  cdlemh  31299  cdlemk5  31318  cdlemk6  31319  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemk21N  31355  cdlemk20  31356  cdlemk28-3  31390  cdlemk34  31392  cdlemkfid3N  31407  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk55u1  31447  cdlemn2  31678  cdlemn10  31689  dihjustlem  31699
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator