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  14940  catass  14941  monpropd  14993  subccocl  15072  funcco  15098  funcpropd  15127  pm2mpmhmlem2  19115  neitr  19475  restutopopn  20504  ustuqtop4  20510  utopreg  20518  cfilucfilOLD  20835  cfilucfil  20836  metutopOLD  20848  psmetutop  20849  dyadmax  21770  tgifscgr  23656  tgcgrxfr  23665  tgbtwnconn1lem3  23716  tgbtwnconn1  23717  legov  23727  legtrd  23731  legso  23740  miriso  23791  perpneq  23827  footex  23831  colperpex  23840  mideulem  23841  mideu  23842  f1otrg  23878  pthdepisspth  24280  clwlkfclwwlk  24548  omndmul2  27392  pstmxmet  27540  lmxrge0  27598  qtophaus  27665  esumcst  27739  signstfvneq0  28197  afsval  28219  heicant  29654  sstotbnd2  29901  eldioph2b  30328  diophren  30379  pell1234qrdich  30429  limcrecl  31199  limclner  31221  icccncfext  31254  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  stoweidlem60  31388  fourierdlem51  31486  fourierdlem77  31512  fourierdlem103  31538  fourierdlem104  31539  iunconlem2  32833
  Copyright terms: Public domain W3C validator