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  17646  catass  17647  monpropd  17699  subccocl  17807  funcco  17833  funcpropd  17864  mhmmnd  18996  ghmqusnsg  19214  ghmquskerlem3  19218  rhmqusnsg  21195  pm2mpmhmlem2  22706  neitr  23067  restutopopn  24126  ustuqtop4  24132  utopreg  24140  cfilucfil  24447  psmetutop  24455  dyadmax  25499  2sqmo  27348  tgifscgr  28435  tgcgrxfr  28445  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  legov  28512  legtrd  28516  legso  28526  miriso  28597  perpneq  28641  footexALT  28645  footex  28648  colperpex  28660  opphllem  28662  midex  28664  opphl  28681  lnopp2hpgb  28690  trgcopyeu  28733  dfcgra2  28757  inaghl  28772  f1otrg  28798  2ndresdju  32573  nn0xmulclb  32694  chnub  32938  omndmul2  33026  psgnfzto1stlem  33057  cyc3genpm  33109  elrgspnlem4  33196  rloccring  33221  rlocf1  33224  dvdsruasso  33356  nsgqusf1olem3  33386  rhmquskerlem  33396  elrspunidl  33399  rhmimaidl  33403  rhmpreimaprmidl  33422  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  ssmxidl  33445  qsdrngi  33466  qsdrng  33468  1arithidom  33508  1arithufdlem3  33517  r1plmhm  33575  r1pquslmic  33576  lbsdiflsp0  33622  fldext2chn  33718  constrconj  33735  constrfin  33736  constrelextdg2  33737  constrfiss  33741  cos9thpiminplylem2  33773  qtophaus  33826  locfinreflem  33830  cmpcref  33840  pstmxmet  33887  lmxrge0  33942  esumcst  34053  omssubadd  34291  signstfvneq0  34563  afsval  34662  matunitlindflem1  37610  heicant  37649  sstotbnd2  37768  primrootscoprmpow  42087  primrootspoweq0  42094  aks6d1c2p2  42107  aks6d1c2lem4  42115  aks6d1c2  42118  unitscyglem3  42185  dffltz  42622  flt4lem7  42647  eldioph2b  42751  diophren  42801  pell1234qrdich  42849  omabs2  43321  iunconnlem2  44924  limcrecl  45627  limclner  45649  icccncfext  45885  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem60  46058  fourierdlem51  46155  fourierdlem77  46181  fourierdlem103  46207  fourierdlem104  46208  smfaddlem1  46761  smfmullem3  46791  grtriprop  47940  upfval  49165  fuco21  49325