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

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

Proof of Theorem simpr33
StepHypRef Expression
1 simp33 1026 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantl 466 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  oppccatid  14781  subccatid  14879  fuccatid  15002  setccatid  15075  catccatid  15093  xpccatid  15121  nllyidm  19235  utoptop  19951  cgr3tr4  28250  paddasslem9  33835  cdlemd1  34205  cdlemf2  34569  cdlemk34  34917  dihmeetlem18N  35332  dihmeetlem19N  35333
  Copyright terms: Public domain W3C validator