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 206  df-an 396

This theorem is referenced by:  catass  17660  mhmmnd  19014  scmatscm  22409  cfilucfil  24462  2sqmo  27364  tgbtwnconn1  28373  legso  28397  footexALT  28516  opphl  28552  trgcopy  28602  dfcgra2  28628  cgrg3col4  28651  f1otrg  28669  2ndresdju  32429  cyc3genpm  32868  cyc3conja  32873  rloccring  32979  rhmquskerlem  33135  rhmqusnsg  33138  rhmimaidl  33143  mxidlirredi  33179  ssmxidllem  33181  r1plmhm  33271  r1pquslmic  33272  pstmxmet  33493  signstfvneq0  34199  afsval  34298  mblfinlem3  37127  mblfinlem4  37128  primrootscoprmpow  41565  aks6d1c2lem4  41593  dffltz  42049  iunconnlem2  44365  suplesup  44712  limclner  45030  fourierdlem51  45536  hoidmvle  45979  smfmullem3  46172