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

Theorem simp1lr 1060
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 755 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th  /\  ta )  ->  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:  lspsolvlem  17914  dmatcrng  19130  scmatcrng  19149  1marepvsma1  19211  mdetunilem7  19246  mat2pmatghm  19357  pmatcollpwscmatlem2  19417  mp2pm2mplem4  19436  ax5seg  24367  measinblem  28352  btwnconn1lem13  29911  pellex  30933  ssfiunibd  31670  mullimc  31783  mullimcf  31790  icccncfext  31851  etransclem32  32210  athgt  35281  llnle  35343  lplnle  35365  lhpexle1  35833  lhpat3  35871  tendoicl  36623  cdlemk55b  36787
  Copyright terms: Public domain W3C validator