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 736	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  17620  catass  17621  monpropd  17673  subccocl  17781  funcco  17807  funcpropd  17838  chnub  18557  mhmmnd  19006  ghmqusnsg  19223  ghmquskerlem3  19227  omndmul2  20074  rhmqusnsg  21252  pm2mpmhmlem2  22775  neitr  23136  restutopopn  24194  ustuqtop4  24200  utopreg  24208  cfilucfil  24515  psmetutop  24523  dyadmax  25567  2sqmo  27416  tgifscgr  28592  tgcgrxfr  28602  tgbtwnconn1lem3  28658  tgbtwnconn1  28659  legov  28669  legtrd  28673  legso  28683  miriso  28754  perpneq  28798  footexALT  28802  footex  28805  colperpex  28817  opphllem  28819  midex  28821  opphl  28838  lnopp2hpgb  28847  trgcopyeu  28890  dfcgra2  28914  inaghl  28929  f1otrg  28955  2ndresdju  32738  nn0xmulclb  32861  psgnfzto1stlem  33193  cyc3genpm  33245  elrgspnlem4  33338  rloccring  33363  rlocf1  33366  dvdsruasso  33477  nsgqusf1olem3  33507  rhmquskerlem  33517  elrspunidl  33520  rhmimaidl  33524  rhmpreimaprmidl  33543  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  mxidlirredi  33563  ssmxidl  33566  qsdrngi  33587  qsdrng  33589  1arithidom  33629  1arithufdlem3  33638  r1plmhm  33702  r1pquslmic  33703  vieta  33756  lbsdiflsp0  33803  fldext2chn  33905  constrconj  33922  constrfin  33923  constrelextdg2  33924  constrfiss  33928  cos9thpiminplylem2  33960  qtophaus  34013  locfinreflem  34017  cmpcref  34027  pstmxmet  34074  lmxrge0  34129  esumcst  34240  omssubadd  34477  signstfvneq0  34749  afsval  34848  matunitlindflem1  37861  heicant  37900  sstotbnd2  38019  primrootscoprmpow  42463  primrootspoweq0  42470  aks6d1c2p2  42483  aks6d1c2lem4  42491  aks6d1c2  42494  unitscyglem3  42561  dffltz  42986  flt4lem7  43011  eldioph2b  43114  diophren  43164  pell1234qrdich  43212  omabs2  43683  iunconnlem2  45284  limcrecl  45983  limclner  46003  icccncfext  46239  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  stoweidlem60  46412  fourierdlem51  46509  fourierdlem77  46535  fourierdlem103  46561  fourierdlem104  46562  smfaddlem1  47115  smfmullem3  47145  chnerlem1  47234  grtriprop  48295  upfval  49529  fuco21  49689