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

Theorem simp-5r 779
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 777 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
21adantr 467 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  simp-6r  781  catcocl  15591  catass  15592  monpropd  15642  subccocl  15750  funcco  15776  funcpropd  15805  mhmmnd  16808  pm2mpmhmlem2  19843  neitr  20196  restutopopn  21253  ustuqtop4  21259  utopreg  21267  cfilucfil  21574  psmetutop  21582  dyadmax  22556  tgifscgr  24553  tgcgrxfr  24563  tgbtwnconn1lem3  24619  tgbtwnconn1  24620  legov  24630  legtrd  24634  legso  24644  miriso  24715  perpneq  24759  footex  24763  colperpex  24775  opphllem  24777  midex  24779  opphl  24796  lnopp2hpgb  24805  trgcopyeu  24848  dfcgra2  24871  inaghl  24881  f1otrg  24901  pthdepisspth  25304  clwlkfclwwlk  25572  2sqmo  28410  omndmul2  28475  psgnfzto1stlem  28613  qtophaus  28663  locfinreflem  28667  cmpcref  28677  pstmxmet  28700  lmxrge0  28758  esumcst  28884  omssubadd  29128  omssubaddOLD  29132  signstfvneq0  29461  afsval  29488  heicant  31975  sstotbnd2  32106  eldioph2b  35605  diophren  35656  pell1234qrdich  35707  iunconlem2  37332  limcrecl  37709  limclner  37732  icccncfext  37765  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  stoweidlem60  37921  fourierdlem51  38021  fourierdlem77  38047  fourierdlem103  38073  fourierdlem104  38074  pthdepissPth  39695
  Copyright terms: Public domain W3C validator