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

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

Proof of Theorem simprl3
StepHypRef Expression
1 simpl3 963 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantl 454 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pwfseqlem5  8540  issubc3  14048  pgpfac1lem5  15639  clscon  17495  txlly  17670  txnlly  17671  itg2add  19653  ftc1a  19923  ax5seglem6  25875  axcontlem10  25914  btwnouttr2  25958  btwnconn1lem13  26035  midofsegid  26040  outsideofeq  26066  ivthALT  26340  icodiamlt  26885  mpaaeu  27334
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator