Theorem simp-5r 831

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 479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad4antr 771	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  simp-6rOLD  836  catcocl  16547  catass  16548  monpropd  16598  subccocl  16706  funcco  16732  funcpropd  16761  mhmmnd  17738  pm2mpmhmlem2  20826  neitr  21186  restutopopn  22243  ustuqtop4  22249  utopreg  22257  cfilucfil  22565  psmetutop  22573  dyadmax  23566  tgifscgr  25602  tgcgrxfr  25612  tgbtwnconn1lem3  25668  tgbtwnconn1  25669  legov  25679  legtrd  25683  legso  25693  miriso  25764  perpneq  25808  footex  25812  colperpex  25824  opphllem  25826  midex  25828  opphl  25845  lnopp2hpgb  25854  trgcopyeu  25897  dfcgra2  25920  inaghl  25930  f1otrg  25950  clwlksfclwwlkOLD  27216  2sqmo  29958  omndmul2  30021  psgnfzto1stlem  30159  qtophaus  30212  locfinreflem  30216  cmpcref  30226  pstmxmet  30249  lmxrge0  30307  esumcst  30434  omssubadd  30671  signstfvneq0  30958  afsval  31058  matunitlindflem1  33718  heicant  33757  sstotbnd2  33886  eldioph2b  37828  diophren  37879  pell1234qrdich  37927  iunconnlem2  39670  limcrecl  40364  limclner  40386  icccncfext  40603  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  stoweidlem60  40780  fourierdlem51  40877  fourierdlem77  40903  fourierdlem103  40929  fourierdlem104  40930  smfaddlem1  41477  smfmullem3  41506