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

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

Proof of Theorem simprl2
StepHypRef Expression
1 simpl2 992 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantl 466 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ps )
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:  issubc3  14771  clscon  19046  txlly  19221  txnlly  19222  itg2add  21249  ftc1a  21521  f1otrg  23129  ax5seglem6  23192  axcontlem9  23230  axcontlem10  23231  erdszelem7  27097  btwnconn1lem13  28142  icodiamlt  29173  clwwlkf  30468  usg2spot2nb  30670
  Copyright terms: Public domain W3C validator