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

Theorem simprl3 1035
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 993 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantl 466 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ch )
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:  pwfseqlem5  8835  issubc3  14764  pgpfac1lem5  16585  clscon  19039  txlly  19214  txnlly  19215  itg2add  21242  ftc1a  21514  f1otrg  23122  ax5seglem6  23185  axcontlem10  23224  btwnouttr2  28058  btwnconn1lem13  28135  midofsegid  28140  outsideofeq  28166  ivthALT  28535  icodiamlt  29166  mpaaeu  29512  numclwwlk5  30710
  Copyright terms: Public domain W3C validator