MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpr31 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  13872  subccatid  13970  fuccatid  14093  setccatid  14166  catccatid  14184  xpccatid  14212  nllyidm  17473  utoptop  18185  cgr3tr4  25700  seglecgr12im  25758  paddasslem9  29942  cdlemd1  30312  cdlemf2  30676  cdlemk34  31024  dihmeetlem18N  31439  dihmeetlem19N  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