Theorem simp-5r 783

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		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 732	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  catcocl  17405  catass  17406  monpropd  17460  subccocl  17571  funcco  17597  funcpropd  17627  mhmmnd  18708  pm2mpmhmlem2  21979  neitr  22342  restutopopn  23401  ustuqtop4  23407  utopreg  23415  cfilucfil  23726  psmetutop  23734  dyadmax  24773  2sqmo  26596  tgifscgr  26880  tgcgrxfr  26890  tgbtwnconn1lem3  26946  tgbtwnconn1  26947  legov  26957  legtrd  26961  legso  26971  miriso  27042  perpneq  27086  footexALT  27090  footex  27093  colperpex  27105  opphllem  27107  midex  27109  opphl  27126  lnopp2hpgb  27135  trgcopyeu  27178  dfcgra2  27202  inaghl  27217  f1otrg  27243  2ndresdju  30995  nn0xmulclb  31103  omndmul2  31347  psgnfzto1stlem  31376  cyc3genpm  31428  nsgqusf1olem3  31609  elrspunidl  31615  rhmimaidl  31618  rhmpreimaprmidl  31636  mxidlprm  31649  ssmxidl  31651  lbsdiflsp0  31716  qtophaus  31795  locfinreflem  31799  cmpcref  31809  pstmxmet  31856  lmxrge0  31911  esumcst  32040  omssubadd  32276  signstfvneq0  32560  afsval  32660  matunitlindflem1  35782  heicant  35821  sstotbnd2  35941  dffltz  40480  flt4lem7  40505  eldioph2b  40594  diophren  40644  pell1234qrdich  40692  iunconnlem2  42537  limcrecl  43152  limclner  43174  icccncfext  43410  ioodvbdlimc1lem2  43455  ioodvbdlimc2lem  43457  stoweidlem60  43583  fourierdlem51  43680  fourierdlem77  43706  fourierdlem103  43732  fourierdlem104  43733  smfaddlem1  44277  smfmullem3  44306