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

Theorem simpr32 1049
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 995 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
21adantl 454 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  oppccatid  13983  subccatid  14081  fuccatid  14204  setccatid  14277  catccatid  14295  xpccatid  14323  nllyidm  17590  utoptop  18302  cgr3tr4  26021  paddasslem9  30799  cdlemd1  31169  cdlemf2  31533  cdlemk34  31881  dihmeetlem18N  32296
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator