Theorem simp-6r 793

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 743	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  catass  17650  chnub  18586  mhmmnd  19038  rhmqusnsg  21285  scmatscm  22503  cfilucfil  24549  2sqmo  27425  tgbtwnconn1  28668  legso  28692  footexALT  28811  opphl  28847  trgcopy  28897  dfcgra2  28923  cgrg3col4  28946  f1otrg  28964  2ndresdju  32748  cyc3genpm  33240  cyc3conja  33245  rloccring  33358  rhmquskerlem  33515  rhmimaidl  33522  ssdifidllem  33546  ssdifidlprm  33548  mxidlirredi  33561  ssmxidllem  33563  1arithidom  33627  1arithufdlem3  33636  r1plmhm  33700  r1pquslmic  33701  fldextrspunlsplem  33864  fldext2chn  33919  constrconj  33936  constrfin  33937  constrelextdg2  33938  cos9thpiminplylem2  33974  pstmxmet  34088  signstfvneq0  34763  afsval  34862  mblfinlem3  38033  mblfinlem4  38034  primrootscoprmpow  42591  aks6d1c2lem4  42619  dffltz  43091  iunconnlem2  45385  suplesup  45791  limclner  46101  fourierdlem51  46607  hoidmvle  47050  smfmullem3  47243  chnerlem1  47334  upfval  49673