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

Theorem simprl2 1042
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 1000 . 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 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:  issubc3  15079  clscon  19737  txlly  19964  txnlly  19965  itg2add  21993  ftc1a  22265  f1otrg  23947  ax5seglem6  24010  axcontlem9  24048  axcontlem10  24049  clwwlkf  24567  usg2spot2nb  24839  erdszelem7  28392  btwnconn1lem13  29602  icodiamlt  30587
  Copyright terms: Public domain W3C validator