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 736	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  17744  mhmmnd  19104  rhmqusnsg  21318  scmatscm  22540  cfilucfil  24593  2sqmo  27499  tgbtwnconn1  28601  legso  28625  footexALT  28744  opphl  28780  trgcopy  28830  dfcgra2  28856  cgrg3col4  28879  f1otrg  28897  2ndresdju  32667  chnub  32984  cyc3genpm  33145  cyc3conja  33150  rloccring  33242  rhmquskerlem  33418  rhmimaidl  33425  ssdifidllem  33449  ssdifidlprm  33451  mxidlirredi  33464  ssmxidllem  33466  1arithidom  33530  1arithufdlem3  33539  r1plmhm  33595  r1pquslmic  33596  fldext2chn  33719  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmxmet  33843  signstfvneq0  34549  afsval  34648  mblfinlem3  37619  mblfinlem4  37620  primrootscoprmpow  42056  aks6d1c2lem4  42084  dffltz  42589  iunconnlem2  44906  suplesup  45254  limclner  45572  fourierdlem51  46078  hoidmvle  46521  smfmullem3  46714