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

Theorem simpr33 1049
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 995 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantl 453 1  |-  ( ( et  /\  ( th 
/\  ta  /\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  oppccatid  13945  subccatid  14043  fuccatid  14166  setccatid  14239  catccatid  14257  xpccatid  14285  nllyidm  17552  utoptop  18264  cgr3tr4  25986  paddasslem9  30625  cdlemd1  30995  cdlemf2  31359  cdlemk34  31707  dihmeetlem18N  32122  dihmeetlem19N  32123
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