Theorem simp-5r 808

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-5r	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		simpr 478	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad4antr 725	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  simp-6rOLD  813  catcocl  16657  catass  16658  monpropd  16708  subccocl  16816  funcco  16842  funcpropd  16871  mhmmnd  17850  pm2mpmhmlem2  20949  neitr  21310  restutopopn  22367  ustuqtop4  22373  utopreg  22381  cfilucfil  22689  psmetutop  22697  dyadmax  23703  tgifscgr  25752  tgcgrxfr  25762  tgbtwnconn1lem3  25818  tgbtwnconn1  25819  legov  25829  legtrd  25833  legso  25843  miriso  25914  perpneq  25958  footex  25962  colperpex  25974  opphllem  25976  midex  25978  opphl  25995  lnopp2hpgb  26004  trgcopyeu  26047  dfcgra2  26070  inaghl  26080  f1otrg  26100  clwlksfclwwlkOLD  27395  2sqmo  30157  omndmul2  30220  psgnfzto1stlem  30358  qtophaus  30411  locfinreflem  30415  cmpcref  30425  pstmxmet  30448  lmxrge0  30506  esumcst  30633  omssubadd  30870  signstfvneq0  31160  afsval  31261  matunitlindflem1  33886  heicant  33925  sstotbnd2  34052  eldioph2b  38100  diophren  38151  pell1234qrdich  38199  iunconnlem2  39919  limcrecl  40593  limclner  40615  icccncfext  40832  ioodvbdlimc1lem2  40879  ioodvbdlimc2lem  40881  stoweidlem60  41008  fourierdlem51  41105  fourierdlem77  41131  fourierdlem103  41157  fourierdlem104  41158  smfaddlem1  41705  smfmullem3  41734