Theorem simp-6r 787

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 737	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  17609  chnub  18545  mhmmnd  18994  rhmqusnsg  21240  scmatscm  22457  cfilucfil  24503  2sqmo  27404  tgbtwnconn1  28647  legso  28671  footexALT  28790  opphl  28826  trgcopy  28876  dfcgra2  28902  cgrg3col4  28925  f1otrg  28943  2ndresdju  32727  cyc3genpm  33234  cyc3conja  33239  rloccring  33352  rhmquskerlem  33506  rhmimaidl  33513  ssdifidllem  33537  ssdifidlprm  33539  mxidlirredi  33552  ssmxidllem  33554  1arithidom  33618  1arithufdlem3  33627  r1plmhm  33691  r1pquslmic  33692  fldextrspunlsplem  33830  fldext2chn  33885  constrconj  33902  constrfin  33903  constrelextdg2  33904  cos9thpiminplylem2  33940  pstmxmet  34054  signstfvneq0  34729  afsval  34828  mblfinlem3  37860  mblfinlem4  37861  primrootscoprmpow  42353  aks6d1c2lem4  42381  dffltz  42877  iunconnlem2  45175  suplesup  45584  limclner  45895  fourierdlem51  46401  hoidmvle  46844  smfmullem3  47037  chnerlem1  47126  upfval  49421