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

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

Proof of Theorem simpr32
StepHypRef Expression
1 simp32 994 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
21adantl 453 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13873  subccatid  13971  fuccatid  14094  setccatid  14167  catccatid  14185  xpccatid  14213  nllyidm  17474  utoptop  18186  cgr3tr4  25701  paddasslem9  29943  cdlemd1  30313  cdlemf2  30677  cdlemk34  31025  dihmeetlem18N  31440
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