Theorem simp-5r 785

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 735	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  catcocl  17608  catass  17609  monpropd  17661  subccocl  17769  funcco  17795  funcpropd  17826  chnub  18545  mhmmnd  18994  ghmqusnsg  19211  ghmquskerlem3  19215  omndmul2  20062  rhmqusnsg  21240  pm2mpmhmlem2  22763  neitr  23124  restutopopn  24182  ustuqtop4  24188  utopreg  24196  cfilucfil  24503  psmetutop  24511  dyadmax  25555  2sqmo  27404  tgifscgr  28580  tgcgrxfr  28590  tgbtwnconn1lem3  28646  tgbtwnconn1  28647  legov  28657  legtrd  28661  legso  28671  miriso  28742  perpneq  28786  footexALT  28790  footex  28793  colperpex  28805  opphllem  28807  midex  28809  opphl  28826  lnopp2hpgb  28835  trgcopyeu  28878  dfcgra2  28902  inaghl  28917  f1otrg  28943  2ndresdju  32727  nn0xmulclb  32851  psgnfzto1stlem  33182  cyc3genpm  33234  elrgspnlem4  33327  rloccring  33352  rlocf1  33355  dvdsruasso  33466  nsgqusf1olem3  33496  rhmquskerlem  33506  elrspunidl  33509  rhmimaidl  33513  rhmpreimaprmidl  33532  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  ssmxidl  33555  qsdrngi  33576  qsdrng  33578  1arithidom  33618  1arithufdlem3  33627  r1plmhm  33691  r1pquslmic  33692  vieta  33736  lbsdiflsp0  33783  fldext2chn  33885  constrconj  33902  constrfin  33903  constrelextdg2  33904  constrfiss  33908  cos9thpiminplylem2  33940  qtophaus  33993  locfinreflem  33997  cmpcref  34007  pstmxmet  34054  lmxrge0  34109  esumcst  34220  omssubadd  34457  signstfvneq0  34729  afsval  34828  matunitlindflem1  37813  heicant  37852  sstotbnd2  37971  primrootscoprmpow  42349  primrootspoweq0  42356  aks6d1c2p2  42369  aks6d1c2lem4  42377  aks6d1c2  42380  unitscyglem3  42447  dffltz  42873  flt4lem7  42898  eldioph2b  43001  diophren  43051  pell1234qrdich  43099  omabs2  43570  iunconnlem2  45171  limcrecl  45871  limclner  45891  icccncfext  46127  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  stoweidlem60  46300  fourierdlem51  46397  fourierdlem77  46423  fourierdlem103  46449  fourierdlem104  46450  smfaddlem1  47003  smfmullem3  47033  chnerlem1  47122  grtriprop  48183  upfval  49417  fuco21  49577