Theorem simp-6r 788

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-6r	⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad6antlr 738	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:  catass  17652  chnub  18588  mhmmnd  19040  rhmqusnsg  21283  scmatscm  22478  cfilucfil  24524  2sqmo  27400  tgbtwnconn1  28643  legso  28667  footexALT  28786  opphl  28822  trgcopy  28872  dfcgra2  28898  cgrg3col4  28921  f1otrg  28939  2ndresdju  32722  cyc3genpm  33213  cyc3conja  33218  rloccring  33331  rhmquskerlem  33485  rhmimaidl  33492  ssdifidllem  33516  ssdifidlprm  33518  mxidlirredi  33531  ssmxidllem  33533  1arithidom  33597  1arithufdlem3  33606  r1plmhm  33670  r1pquslmic  33671  fldextrspunlsplem  33817  fldext2chn  33872  constrconj  33889  constrfin  33890  constrelextdg2  33891  cos9thpiminplylem2  33927  pstmxmet  34041  signstfvneq0  34716  afsval  34815  mblfinlem3  37980  mblfinlem4  37981  primrootscoprmpow  42538  aks6d1c2lem4  42566  dffltz  43067  iunconnlem2  45361  suplesup  45769  limclner  46079  fourierdlem51  46585  hoidmvle  47028  smfmullem3  47221  chnerlem1  47312  upfval  49651