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

Theorem simprl2 1051
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 1009 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantl 467 1  |-  ( ( ta  /\  ( (
ph  /\  ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  issubc3  15698  clscon  20369  txlly  20575  txnlly  20576  itg2add  22591  ftc1a  22863  f1otrg  24744  ax5seglem6  24807  axcontlem9  24845  axcontlem10  24846  clwwlkf  25364  usg2spot2nb  25635  locfinref  28504  erdszelem7  29705  btwnconn1lem13  30648  icodiamlt  35374
  Copyright terms: Public domain W3C validator