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

Theorem simpr3l 1016
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 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantl 452 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seg  24566  axcont  24604  segconeq  24633  idinside  24707  btwnconn1lem10  24719  segletr  24737  stoweidlem56  27805  cdlemc3  30382  cdlemc4  30383  cdleme1  30416  cdleme2  30417  cdleme3b  30418  cdleme3c  30419  cdleme3e  30421  cdleme27a  30556
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