Theorem simp-5r 786

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  17728  catass  17729  monpropd  17781  subccocl  17890  funcco  17916  funcpropd  17947  mhmmnd  19082  ghmqusnsg  19300  ghmquskerlem3  19304  rhmqusnsg  21295  pm2mpmhmlem2  22825  neitr  23188  restutopopn  24247  ustuqtop4  24253  utopreg  24261  cfilucfil  24572  psmetutop  24580  dyadmax  25633  2sqmo  27481  tgifscgr  28516  tgcgrxfr  28526  tgbtwnconn1lem3  28582  tgbtwnconn1  28583  legov  28593  legtrd  28597  legso  28607  miriso  28678  perpneq  28722  footexALT  28726  footex  28729  colperpex  28741  opphllem  28743  midex  28745  opphl  28762  lnopp2hpgb  28771  trgcopyeu  28814  dfcgra2  28838  inaghl  28853  f1otrg  28879  2ndresdju  32659  nn0xmulclb  32775  chnub  33002  omndmul2  33089  psgnfzto1stlem  33120  cyc3genpm  33172  elrgspnlem4  33249  rloccring  33274  rlocf1  33277  dvdsruasso  33413  nsgqusf1olem3  33443  rhmquskerlem  33453  elrspunidl  33456  rhmimaidl  33460  rhmpreimaprmidl  33479  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  ssmxidl  33502  qsdrngi  33523  qsdrng  33525  1arithidom  33565  1arithufdlem3  33574  r1plmhm  33630  r1pquslmic  33631  lbsdiflsp0  33677  fldext2chn  33769  constrconj  33786  constrfin  33787  constrelextdg2  33788  qtophaus  33835  locfinreflem  33839  cmpcref  33849  pstmxmet  33896  lmxrge0  33951  esumcst  34064  omssubadd  34302  signstfvneq0  34587  afsval  34686  matunitlindflem1  37623  heicant  37662  sstotbnd2  37781  primrootscoprmpow  42100  primrootspoweq0  42107  aks6d1c2p2  42120  aks6d1c2lem4  42128  aks6d1c2  42131  unitscyglem3  42198  dffltz  42644  flt4lem7  42669  eldioph2b  42774  diophren  42824  pell1234qrdich  42872  omabs2  43345  iunconnlem2  44955  limcrecl  45644  limclner  45666  icccncfext  45902  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem60  46075  fourierdlem51  46172  fourierdlem77  46198  fourierdlem103  46224  fourierdlem104  46225  smfaddlem1  46778  smfmullem3  46808  grtriprop  47908  upfval  48933  fuco21  49031