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

Theorem simp22r 1150
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 1057 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 1052 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  ax5seglem6  25043  segconeu  30849  3atlem2  33120  lplnexllnN  33200  lplncvrlvol2  33251  4atex  33712  cdleme3g  33871  cdleme3h  33872  cdleme11h  33903  cdleme20bN  33948  cdleme20c  33949  cdleme20f  33952  cdleme20g  33953  cdleme20j  33956  cdleme20l2  33959  cdleme20l  33960  cdleme21ct  33967  cdleme26e  33997  cdleme43fsv1snlem  34058  cdleme39n  34104  cdleme40m  34105  cdleme42k  34122  cdlemg6c  34258  cdlemg31d  34338  cdlemg33a  34344  cdlemg33c  34346  cdlemg33d  34347  cdlemg33e  34348  cdlemg33  34349  cdlemh  34455  cdlemk7u-2N  34526  cdlemk11u-2N  34527  cdlemk12u-2N  34528  cdlemk20-2N  34530  cdlemk28-3  34546  cdlemk33N  34547  cdlemk34  34548  cdlemk39  34554  cdlemkyyN  34600
  Copyright terms: Public domain W3C validator