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 787
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 785 . 2  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
21adantr 472 1  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  simp-6r  789  catcocl  15669  catass  15670  monpropd  15720  subccocl  15828  funcco  15854  funcpropd  15883  mhmmnd  16886  pm2mpmhmlem2  19920  neitr  20273  restutopopn  21331  ustuqtop4  21337  utopreg  21345  cfilucfil  21652  psmetutop  21660  dyadmax  22635  tgifscgr  24632  tgcgrxfr  24642  tgbtwnconn1lem3  24698  tgbtwnconn1  24699  legov  24709  legtrd  24713  legso  24723  miriso  24794  perpneq  24838  footex  24842  colperpex  24854  opphllem  24856  midex  24858  opphl  24875  lnopp2hpgb  24884  trgcopyeu  24927  dfcgra2  24950  inaghl  24960  f1otrg  24980  pthdepisspth  25383  clwlkfclwwlk  25651  2sqmo  28485  omndmul2  28549  psgnfzto1stlem  28687  qtophaus  28737  locfinreflem  28741  cmpcref  28751  pstmxmet  28774  lmxrge0  28832  esumcst  28958  omssubadd  29201  omssubaddOLD  29205  signstfvneq0  29533  afsval  29560  heicant  32039  sstotbnd2  32170  eldioph2b  35676  diophren  35727  pell1234qrdich  35778  iunconlem2  37395  limcrecl  37806  limclner  37829  icccncfext  37862  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  stoweidlem60  38033  fourierdlem51  38133  fourierdlem77  38159  fourierdlem103  38185  fourierdlem104  38186  pthdepissPth  39927
  Copyright terms: Public domain W3C validator