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  17651  catass  17652  monpropd  17704  subccocl  17812  funcco  17838  funcpropd  17869  chnub  18588  mhmmnd  19040  ghmqusnsg  19257  ghmquskerlem3  19261  omndmul2  20108  rhmqusnsg  21283  pm2mpmhmlem2  22784  neitr  23145  restutopopn  24203  ustuqtop4  24209  utopreg  24217  cfilucfil  24524  psmetutop  24532  dyadmax  25565  2sqmo  27400  tgifscgr  28576  tgcgrxfr  28586  tgbtwnconn1lem3  28642  tgbtwnconn1  28643  legov  28653  legtrd  28657  legso  28667  miriso  28738  perpneq  28782  footexALT  28786  footex  28789  colperpex  28801  opphllem  28803  midex  28805  opphl  28822  lnopp2hpgb  28831  trgcopyeu  28874  dfcgra2  28898  inaghl  28913  f1otrg  28939  2ndresdju  32722  nn0xmulclb  32844  psgnfzto1stlem  33161  cyc3genpm  33213  elrgspnlem4  33306  rloccring  33331  rlocf1  33334  dvdsruasso  33445  nsgqusf1olem3  33475  rhmquskerlem  33485  elrspunidl  33488  rhmimaidl  33492  rhmpreimaprmidl  33511  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  ssmxidl  33534  qsdrngi  33555  qsdrng  33557  1arithidom  33597  1arithufdlem3  33606  r1plmhm  33670  r1pquslmic  33671  vieta  33724  lbsdiflsp0  33770  fldext2chn  33872  constrconj  33889  constrfin  33890  constrelextdg2  33891  constrfiss  33895  cos9thpiminplylem2  33927  qtophaus  33980  locfinreflem  33984  cmpcref  33994  pstmxmet  34041  lmxrge0  34096  esumcst  34207  omssubadd  34444  signstfvneq0  34716  afsval  34815  matunitlindflem1  37937  heicant  37976  sstotbnd2  38095  primrootscoprmpow  42538  primrootspoweq0  42545  aks6d1c2p2  42558  aks6d1c2lem4  42566  aks6d1c2  42569  unitscyglem3  42636  dffltz  43067  flt4lem7  43092  eldioph2b  43195  diophren  43241  pell1234qrdich  43289  omabs2  43760  iunconnlem2  45361  limcrecl  46059  limclner  46079  icccncfext  46315  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem60  46488  fourierdlem51  46585  fourierdlem77  46611  fourierdlem103  46637  fourierdlem104  46638  smfaddlem1  47191  smfmullem3  47221  chnerlem1  47312  grtriprop  48417  upfval  49651  fuco21  49811