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

Theorem simp-5r 777
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 775 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
21adantr 466 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  simp-6r  779  catcocl  15535  catass  15536  monpropd  15586  subccocl  15694  funcco  15720  funcpropd  15749  mhmmnd  16752  pm2mpmhmlem2  19767  neitr  20120  restutopopn  21177  ustuqtop4  21183  utopreg  21191  cfilucfil  21498  psmetutop  21506  dyadmax  22450  tgifscgr  24442  tgcgrxfr  24451  tgbtwnconn1lem3  24505  tgbtwnconn1  24506  legov  24516  legtrd  24520  legso  24530  miriso  24600  perpneq  24642  footex  24646  colperpex  24658  opphllem  24660  midex  24662  opphl  24679  lnopp2hpgb  24687  trgcopyeu  24730  dfcgra2  24752  f1otrg  24773  pthdepisspth  25175  clwlkfclwwlk  25443  2sqmo  28274  omndmul2  28339  psgnfzto1stlem  28478  qtophaus  28528  locfinreflem  28532  cmpcref  28542  pstmxmet  28565  lmxrge0  28623  esumcst  28749  omssubadd  28987  signstfvneq0  29275  afsval  29302  heicant  31708  sstotbnd2  31839  eldioph2b  35343  diophren  35394  pell1234qrdich  35446  iunconlem2  37005  limcrecl  37314  limclner  37337  icccncfext  37370  ioodvbdlimc1lem2  37409  ioodvbdlimc2lem  37411  stoweidlem60  37523  fourierdlem51  37622  fourierdlem77  37648  fourierdlem103  37674  fourierdlem104  37675
  Copyright terms: Public domain W3C validator