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

Theorem simp21r 1123
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 1030 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 1027 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  modexp  12406  segconeu  30770  4atlem10  33089  lplncvrlvol2  33098  4atex  33559  4atex2-0cOLDN  33563  cdleme0moN  33709  cdleme16e  33766  cdleme17d1  33773  cdleme18d  33779  cdleme19d  33791  cdleme20f  33799  cdleme20g  33800  cdleme21ct  33814  cdleme22aa  33824  cdleme22cN  33827  cdleme22d  33828  cdleme22e  33829  cdleme22eALTN  33830  cdleme26e  33844  cdleme32e  33930  cdleme32f  33931  cdlemg4  34102  cdlemg18d  34166  cdlemg18  34167  cdlemg19a  34168  cdlemg19  34169  cdlemg21  34171  cdlemg33b0  34186  cdlemk5  34321  cdlemk6  34322  cdlemk7  34333  cdlemk11  34334  cdlemk12  34335  cdlemk21N  34358  cdlemk20  34359  cdlemk28-3  34393  cdlemk34  34395  cdlemkfid3N  34410  cdlemk55u1  34450
  Copyright terms: Public domain W3C validator