MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-5r Unicode version

Theorem simp-5r 746
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-5r  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )

Proof of Theorem simp-5r
StepHypRef Expression
1 simp-4r 744 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
21adantr 452 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-6r  748  catcocl  13837  catass  13838  monpropd  13890  subccocl  13969  funcco  13995  funcpropd  14024  neitr  17166  restutopopn  18189  ustuqtop4  18195  utopreg  18203  cfilucfil  18479  metutop  18487  dyadmax  19357  pthdepisspth  21428  lmxrge0  24141  esumcst  24251  sstotbnd2  26174  eldioph2b  26512  diophren  26565  pell1234qrdich  26615  stoweidlem60  27477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator