MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp21r Structured version   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  11504  segconeu  25910  4atlem10  30304  lplncvrlvol2  30313  4atex  30774  4atex2-0cOLDN  30778  cdleme0moN  30923  cdleme16e  30980  cdleme17d1  30987  cdleme18d  30993  cdleme19d  31004  cdleme20f  31012  cdleme20g  31013  cdleme21ct  31027  cdleme22aa  31037  cdleme22cN  31040  cdleme22d  31041  cdleme22e  31042  cdleme22eALTN  31043  cdleme26e  31057  cdleme32e  31143  cdleme32f  31144  cdlemg4  31315  cdlemg18d  31379  cdlemg18  31380  cdlemg19a  31381  cdlemg19  31382  cdlemg21  31384  cdlemg33b0  31399  cdlemk5  31534  cdlemk6  31535  cdlemk7  31546  cdlemk11  31547  cdlemk12  31548  cdlemk21N  31571  cdlemk20  31572  cdlemk28-3  31606  cdlemk34  31608  cdlemkfid3N  31623  cdlemk55u1  31663
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