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

Theorem simpr3l 1019
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantl 454 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ax5seg  25882  axcont  25920  segconeq  25949  idinside  26023  btwnconn1lem10  26035  segletr  26053  stoweidlem56  27795  cdlemc3  31064  cdlemc4  31065  cdleme1  31098  cdleme2  31099  cdleme3b  31100  cdleme3c  31101  cdleme3e  31103  cdleme27a  31238
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator