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  17697  catass  17698  monpropd  17750  subccocl  17858  funcco  17884  funcpropd  17915  mhmmnd  19047  ghmqusnsg  19265  ghmquskerlem3  19269  rhmqusnsg  21246  pm2mpmhmlem2  22757  neitr  23118  restutopopn  24177  ustuqtop4  24183  utopreg  24191  cfilucfil  24498  psmetutop  24506  dyadmax  25551  2sqmo  27400  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  32627  nn0xmulclb  32748  chnub  32992  omndmul2  33080  psgnfzto1stlem  33111  cyc3genpm  33163  elrgspnlem4  33240  rloccring  33265  rlocf1  33268  dvdsruasso  33400  nsgqusf1olem3  33430  rhmquskerlem  33440  elrspunidl  33443  rhmimaidl  33447  rhmpreimaprmidl  33466  ssdifidllem  33471  ssdifidlprm  33473  mxidlprm  33485  mxidlirredi  33486  ssmxidl  33489  qsdrngi  33510  qsdrng  33512  1arithidom  33552  1arithufdlem3  33561  r1plmhm  33619  r1pquslmic  33620  lbsdiflsp0  33666  fldext2chn  33762  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrfiss  33785  cos9thpiminplylem2  33817  qtophaus  33867  locfinreflem  33871  cmpcref  33881  pstmxmet  33928  lmxrge0  33983  esumcst  34094  omssubadd  34332  signstfvneq0  34604  afsval  34703  matunitlindflem1  37640  heicant  37679  sstotbnd2  37798  primrootscoprmpow  42112  primrootspoweq0  42119  aks6d1c2p2  42132  aks6d1c2lem4  42140  aks6d1c2  42143  unitscyglem3  42210  dffltz  42657  flt4lem7  42682  eldioph2b  42786  diophren  42836  pell1234qrdich  42884  omabs2  43356  iunconnlem2  44959  limcrecl  45658  limclner  45680  icccncfext  45916  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweidlem60  46089  fourierdlem51  46186  fourierdlem77  46212  fourierdlem103  46238  fourierdlem104  46239  smfaddlem1  46792  smfmullem3  46822  grtriprop  47953  upfval  49111  fuco21  49247