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

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

Proof of Theorem simpr3l
StepHypRef Expression
1 simp3l 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantl 453 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ax5seg  25789  axcont  25827  segconeq  25856  idinside  25930  btwnconn1lem10  25942  segletr  25960  stoweidlem56  27680  cdlemc3  30687  cdlemc4  30688  cdleme1  30721  cdleme2  30722  cdleme3b  30723  cdleme3c  30724  cdleme3e  30726  cdleme27a  30861
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