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

Theorem simprl3 1044
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 1002 . 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 974
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 976
This theorem is referenced by:  pwfseqlem5  9044  issubc3  15197  pgpfac1lem5  17109  clscon  19909  txlly  20115  txnlly  20116  itg2add  22144  ftc1a  22416  f1otrg  24152  ax5seglem6  24215  axcontlem10  24254  numclwwlk5  25090  locfinref  27822  btwnouttr2  29648  btwnconn1lem13  29725  midofsegid  29730  outsideofeq  29756  ivthALT  30129  icodiamlt  30732  mpaaeu  31075
  Copyright terms: Public domain W3C validator