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  17621  chnub  18557  mhmmnd  19006  rhmqusnsg  21252  scmatscm  22469  cfilucfil  24515  2sqmo  27416  tgbtwnconn1  28659  legso  28683  footexALT  28802  opphl  28838  trgcopy  28888  dfcgra2  28914  cgrg3col4  28937  f1otrg  28955  2ndresdju  32738  cyc3genpm  33245  cyc3conja  33250  rloccring  33363  rhmquskerlem  33517  rhmimaidl  33524  ssdifidllem  33548  ssdifidlprm  33550  mxidlirredi  33563  ssmxidllem  33565  1arithidom  33629  1arithufdlem3  33638  r1plmhm  33702  r1pquslmic  33703  fldextrspunlsplem  33850  fldext2chn  33905  constrconj  33922  constrfin  33923  constrelextdg2  33924  cos9thpiminplylem2  33960  pstmxmet  34074  signstfvneq0  34749  afsval  34848  mblfinlem3  37907  mblfinlem4  37908  primrootscoprmpow  42466  aks6d1c2lem4  42494  dffltz  42989  iunconnlem2  45287  suplesup  45695  limclner  46006  fourierdlem51  46512  hoidmvle  46955  smfmullem3  47148  chnerlem1  47237  upfval  49532