MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-5r Structured version   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  13902  catass  13903  monpropd  13955  subccocl  14034  funcco  14060  funcpropd  14089  neitr  17236  restutopopn  18260  ustuqtop4  18266  utopreg  18274  cfilucfilOLD  18591  cfilucfil  18592  metutopOLD  18604  psmetutop  18605  dyadmax  19482  pthdepisspth  21566  pstmxmet  24284  lmxrge0  24329  esumcst  24447  sstotbnd2  26464  eldioph2b  26802  diophren  26855  pell1234qrdich  26905  stoweidlem60  27766  iunconlem2  28974
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