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

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

Proof of Theorem simp22r
StepHypRef Expression
1 simp2r 1015 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  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:  ax5seglem6  23317  segconeu  28178  3atlem2  33436  lplnexllnN  33516  lplncvrlvol2  33567  4atex  34028  cdleme3g  34186  cdleme3h  34187  cdleme11h  34218  cdleme20bN  34262  cdleme20c  34263  cdleme20f  34266  cdleme20g  34267  cdleme20j  34270  cdleme20l2  34273  cdleme20l  34274  cdleme21ct  34281  cdleme26e  34311  cdleme43fsv1snlem  34372  cdleme39n  34418  cdleme40m  34419  cdleme42k  34436  cdlemg6c  34572  cdlemg31d  34652  cdlemg33a  34658  cdlemg33c  34660  cdlemg33d  34661  cdlemg33e  34662  cdlemg33  34663  cdlemh  34769  cdlemk7u-2N  34840  cdlemk11u-2N  34841  cdlemk12u-2N  34842  cdlemk20-2N  34844  cdlemk28-3  34860  cdlemk33N  34861  cdlemk34  34862  cdlemk39  34868  cdlemkyyN  34914
  Copyright terms: Public domain W3C validator