Theorem simp-5r 791

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 741	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 208  df-an 397

This theorem is referenced by:  catcocl  17649  catass  17650  monpropd  17702  subccocl  17810  funcco  17836  funcpropd  17867  chnub  18586  mhmmnd  19038  ghmqusnsg  19255  ghmquskerlem3  19259  omndmul2  20106  rhmqusnsg  21285  pm2mpmhmlem2  22809  neitr  23170  restutopopn  24228  ustuqtop4  24234  utopreg  24242  cfilucfil  24549  psmetutop  24557  dyadmax  25590  2sqmo  27425  tgifscgr  28601  tgcgrxfr  28611  tgbtwnconn1lem3  28667  tgbtwnconn1  28668  legov  28678  legtrd  28682  legso  28692  miriso  28763  perpneq  28807  footexALT  28811  footex  28814  colperpex  28826  opphllem  28828  midex  28830  opphl  28847  lnopp2hpgb  28856  trgcopyeu  28899  dfcgra2  28923  inaghl  28938  f1otrg  28964  2ndresdju  32748  nn0xmulclb  32870  psgnfzto1stlem  33188  cyc3genpm  33240  elrgspnlem4  33333  rloccring  33358  rlocf1  33361  ricdomn1  33377  dvdsruasso  33475  nsgqusf1olem3  33505  rhmquskerlem  33515  elrspunidl  33518  rhmimaidl  33522  rhmpreimaprmidl  33541  ssdifidllem  33546  ssdifidlprm  33548  mxidlprm  33560  mxidlirredi  33561  ssmxidl  33564  qsdrngi  33585  qsdrng  33587  1arithidom  33627  1arithufdlem3  33636  r1plmhm  33700  r1pquslmic  33701  mplidomlem  33718  vieta  33771  lbsdiflsp0  33817  fldext2chn  33919  constrconj  33936  constrfin  33937  constrelextdg2  33938  constrfiss  33942  cos9thpiminplylem2  33974  qtophaus  34027  locfinreflem  34031  cmpcref  34041  pstmxmet  34088  lmxrge0  34143  esumcst  34254  omssubadd  34491  signstfvneq0  34763  afsval  34862  matunitlindflem1  37990  heicant  38029  sstotbnd2  38148  primrootscoprmpow  42591  primrootspoweq0  42598  aks6d1c2p2  42611  aks6d1c2lem4  42619  aks6d1c2  42622  unitscyglem3  42689  dffltz  43091  flt4lem7  43116  eldioph2b  43219  diophren  43265  pell1234qrdich  43313  omabs2  43784  iunconnlem2  45385  limcrecl  46081  limclner  46101  icccncfext  46337  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem60  46510  fourierdlem51  46607  fourierdlem77  46633  fourierdlem103  46659  fourierdlem104  46660  smfaddlem1  47213  smfmullem3  47243  chnerlem1  47334  grtriprop  48439  upfval  49673  fuco21  49833