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

Theorem simpr33 1086
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 1032 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantl 464 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  oppccatid  15207  subccatid  15334  fuccatid  15457  setccatid  15562  catccatid  15580  estrccatid  15600  xpccatid  15656  nllyidm  20156  utoptop  20903  cgr3tr4  29930  paddasslem9  35949  cdlemd1  36320  cdlemf2  36685  cdlemk34  37033  dihmeetlem18N  37448  dihmeetlem19N  37449
  Copyright terms: Public domain W3C validator