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

Theorem simp-5r 768
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 766 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
21adantr 465 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  simp-6r  770  catcocl  14628  catass  14629  monpropd  14681  subccocl  14760  funcco  14786  funcpropd  14815  neitr  18789  restutopopn  19818  ustuqtop4  19824  utopreg  19832  cfilucfilOLD  20149  cfilucfil  20150  metutopOLD  20162  psmetutop  20163  dyadmax  21083  tgifscgr  22966  tgcgrxfr  22975  tgbtwnconn1lem3  23011  tgbtwnconn1  23012  legov  23021  legtrd  23025  miriso  23078  perpneq  23110  footex  23114  f1otrg  23122  pthdepisspth  23478  omndmul2  26180  pstmxmet  26329  lmxrge0  26387  esumcst  26519  signstfvneq0  26978  afsval  27000  heicant  28431  sstotbnd2  28678  eldioph2b  29106  diophren  29157  pell1234qrdich  29207  stoweidlem60  29860  clwlkfclwwlk  30522  pmatcollpw1dst  30906  iunconlem2  31676
  Copyright terms: Public domain W3C validator