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

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

Proof of Theorem simpr31
StepHypRef Expression
1 simp31 993 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantl 453 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13937  subccatid  14035  fuccatid  14158  setccatid  14231  catccatid  14249  xpccatid  14277  nllyidm  17544  utoptop  18256  cgr3tr4  25978  seglecgr12im  26036  paddasslem9  30552  cdlemd1  30922  cdlemf2  31286  cdlemk34  31634  dihmeetlem18N  32049  dihmeetlem19N  32050
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