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

Theorem simpr3l 1017
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 984 . 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 935
This theorem is referenced by:  ax5seg  25308  axcont  25346  segconeq  25375  idinside  25449  btwnconn1lem10  25461  segletr  25479  stoweidlem56  27311  cdlemc3  30453  cdlemc4  30454  cdleme1  30487  cdleme2  30488  cdleme3b  30489  cdleme3c  30490  cdleme3e  30492  cdleme27a  30627
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 937
  Copyright terms: Public domain W3C validator