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

Theorem simp21r 1075
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 979 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  modexp  11502  segconeu  25893  4atlem10  30242  lplncvrlvol2  30251  4atex  30712  4atex2-0cOLDN  30716  cdleme0moN  30861  cdleme16e  30918  cdleme17d1  30925  cdleme18d  30931  cdleme19d  30942  cdleme20f  30950  cdleme20g  30951  cdleme21ct  30965  cdleme22aa  30975  cdleme22cN  30978  cdleme22d  30979  cdleme22e  30980  cdleme22eALTN  30981  cdleme26e  30995  cdleme32e  31081  cdleme32f  31082  cdlemg4  31253  cdlemg18d  31317  cdlemg18  31318  cdlemg19a  31319  cdlemg19  31320  cdlemg21  31322  cdlemg33b0  31337  cdlemk5  31472  cdlemk6  31473  cdlemk7  31484  cdlemk11  31485  cdlemk12  31486  cdlemk21N  31509  cdlemk20  31510  cdlemk28-3  31544  cdlemk34  31546  cdlemkfid3N  31561  cdlemk55u1  31601
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