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

Theorem simp21r 1106
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 1013 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  modexp  12100  segconeu  28176  4atlem10  33556  lplncvrlvol2  33565  4atex  34026  4atex2-0cOLDN  34030  cdleme0moN  34175  cdleme16e  34232  cdleme17d1  34239  cdleme18d  34245  cdleme19d  34256  cdleme20f  34264  cdleme20g  34265  cdleme21ct  34279  cdleme22aa  34289  cdleme22cN  34292  cdleme22d  34293  cdleme22e  34294  cdleme22eALTN  34295  cdleme26e  34309  cdleme32e  34395  cdleme32f  34396  cdlemg4  34567  cdlemg18d  34631  cdlemg18  34632  cdlemg19a  34633  cdlemg19  34634  cdlemg21  34636  cdlemg33b0  34651  cdlemk5  34786  cdlemk6  34787  cdlemk7  34798  cdlemk11  34799  cdlemk12  34800  cdlemk21N  34823  cdlemk20  34824  cdlemk28-3  34858  cdlemk34  34860  cdlemkfid3N  34875  cdlemk55u1  34915
  Copyright terms: Public domain W3C validator