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

Theorem simpr31 1045
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 991 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantl 452 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  oppccatid  13622  subccatid  13720  fuccatid  13843  setccatid  13916  catccatid  13934  xpccatid  13962  nllyidm  17215  cgr3tr4  24675  seglecgr12im  24733  injsurinj  25149  paddasslem9  30017  cdlemd1  30387  cdlemf2  30751  cdlemk34  31099  dihmeetlem18N  31514  dihmeetlem19N  31515
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator