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  17593  catass  17594  monpropd  17646  subccocl  17754  funcco  17780  funcpropd  17811  chnub  18530  mhmmnd  18979  ghmqusnsg  19196  ghmquskerlem3  19200  omndmul2  20047  rhmqusnsg  21224  pm2mpmhmlem2  22735  neitr  23096  restutopopn  24154  ustuqtop4  24160  utopreg  24168  cfilucfil  24475  psmetutop  24483  dyadmax  25527  2sqmo  27376  tgifscgr  28487  tgcgrxfr  28497  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  legov  28564  legtrd  28568  legso  28578  miriso  28649  perpneq  28693  footexALT  28697  footex  28700  colperpex  28712  opphllem  28714  midex  28716  opphl  28733  lnopp2hpgb  28742  trgcopyeu  28785  dfcgra2  28809  inaghl  28824  f1otrg  28850  2ndresdju  32633  nn0xmulclb  32758  psgnfzto1stlem  33076  cyc3genpm  33128  elrgspnlem4  33219  rloccring  33244  rlocf1  33247  dvdsruasso  33357  nsgqusf1olem3  33387  rhmquskerlem  33397  elrspunidl  33400  rhmimaidl  33404  rhmpreimaprmidl  33423  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  mxidlirredi  33443  ssmxidl  33446  qsdrngi  33467  qsdrng  33469  1arithidom  33509  1arithufdlem3  33518  r1plmhm  33577  r1pquslmic  33578  lbsdiflsp0  33660  fldext2chn  33762  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrfiss  33785  cos9thpiminplylem2  33817  qtophaus  33870  locfinreflem  33874  cmpcref  33884  pstmxmet  33931  lmxrge0  33986  esumcst  34097  omssubadd  34334  signstfvneq0  34606  afsval  34705  matunitlindflem1  37676  heicant  37715  sstotbnd2  37834  primrootscoprmpow  42212  primrootspoweq0  42219  aks6d1c2p2  42232  aks6d1c2lem4  42240  aks6d1c2  42243  unitscyglem3  42310  dffltz  42752  flt4lem7  42777  eldioph2b  42880  diophren  42930  pell1234qrdich  42978  omabs2  43449  iunconnlem2  45051  limcrecl  45753  limclner  45773  icccncfext  46009  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  stoweidlem60  46182  fourierdlem51  46279  fourierdlem77  46305  fourierdlem103  46331  fourierdlem104  46332  smfaddlem1  46885  smfmullem3  46915  chnerlem1  47004  grtriprop  48065  upfval  49301  fuco21  49461