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

Theorem simprl3 1043
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 1001 . 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 973
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 975
This theorem is referenced by:  pwfseqlem5  9041  issubc3  15076  pgpfac1lem5  16932  clscon  19725  txlly  19900  txnlly  19901  itg2add  21929  ftc1a  22201  f1otrg  23878  ax5seglem6  23941  axcontlem10  23980  numclwwlk5  24817  btwnouttr2  29277  btwnconn1lem13  29354  midofsegid  29359  outsideofeq  29385  ivthALT  29758  icodiamlt  30388  mpaaeu  30732
  Copyright terms: Public domain W3C validator