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

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

Proof of Theorem simp1lr
StepHypRef Expression
1 simplr 754 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  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:  lspsolvlem  17228  1marepvsma1  18399  mdetunilem7  18429  ax5seg  23189  measinblem  26639  btwnconn1lem13  28135  pellex  29181  dmatcrng  30886  scmatcrng  30893  mp2pm2mplem4  30924  athgt  33105  llnle  33167  lplnle  33189  lhpexle1  33657  lhpat3  33695  tendoicl  34445  cdlemk55b  34609
  Copyright terms: Public domain W3C validator