Theorem simp-6r 799

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad6antlr 749	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  catass  17730  chnub  18666  mhmmnd  19118  rhmqusnsg  21384  ssdifidllem  21441  ssdifidlprm  21443  scmatscm  22627  cfilucfil  24673  2sqmo  27555  tgbtwnconn1  28798  legso  28822  footexALT  28945  opphl  28981  trgcopy  29052  dfcgra2  29078  cgrg3col4  29101  f1otrg  29125  2ndresdju  32902  cyc3genpm  33380  cyc3conja  33385  rloccring  33499  rhmquskerlem  33644  rhmimaidl  33651  mxidlirredi  33666  ssmxidllem  33668  1arithidom  33739  1arithufdlem3  33748  r1plmhm  33811  r1pquslmic  33812  fldextrspunlsplem  33975  fldext2chn  34030  constrconj  34047  constrfin  34048  constrelextdg2  34049  cos9thpiminplylem2  34085  pstmxmet  34199  signstfvneq0  34871  afsval  34973  mblfinlem3  38165  mblfinlem4  38166  primrootscoprmpow  42723  aks6d1c2lem4  42751  dffltz  43223  iunconnlem2  45502  suplesup  45914  limclner  46224  fourierdlem51  46730  hoidmvle  47173  smfmullem3  47366  chnerlem1  47457  upfval  49806