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

Theorem simp21r 1076
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21r  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 983 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 980 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  modexp  11519  segconeu  25950  4atlem10  30477  lplncvrlvol2  30486  4atex  30947  4atex2-0cOLDN  30951  cdleme0moN  31096  cdleme16e  31153  cdleme17d1  31160  cdleme18d  31166  cdleme19d  31177  cdleme20f  31185  cdleme20g  31186  cdleme21ct  31200  cdleme22aa  31210  cdleme22cN  31213  cdleme22d  31214  cdleme22e  31215  cdleme22eALTN  31216  cdleme26e  31230  cdleme32e  31316  cdleme32f  31317  cdlemg4  31488  cdlemg18d  31552  cdlemg18  31553  cdlemg19a  31554  cdlemg19  31555  cdlemg21  31557  cdlemg33b0  31572  cdlemk5  31707  cdlemk6  31708  cdlemk7  31719  cdlemk11  31720  cdlemk12  31721  cdlemk21N  31744  cdlemk20  31745  cdlemk28-3  31779  cdlemk34  31781  cdlemkfid3N  31796  cdlemk55u1  31836
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator