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

Theorem simpr3l 1049
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 1016 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantl 466 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) ) )  ->  ph )
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:  ax5seg  23363  axcont  23401  segconeq  28208  idinside  28282  btwnconn1lem10  28294  segletr  28312  stoweidlem56  30022  cdlemc3  34200  cdlemc4  34201  cdleme1  34234  cdleme2  34235  cdleme3b  34236  cdleme3c  34237  cdleme3e  34239  cdleme27a  34374
  Copyright terms: Public domain W3C validator