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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  catass  17060  mhmmnd  18339  scmatscm  21264  cfilucfil  23312  2sqmo  26173  istrkgb  26401  istrkge  26403  tgbtwnconn1  26521  legso  26545  footexALT  26664  opphl  26700  trgcopy  26750  dfcgra2  26776  cgrg3col4  26799  f1otrg  26817  2ndresdju  30560  cyc3genpm  30996  cyc3conja  31001  rhmimaidl  31181  ssmxidllem  31213  pstmxmet  31419  signstfvneq0  32121  afsval  32221  mblfinlem3  35439  mblfinlem4  35440  dffltz  40043  iunconnlem2  42093  suplesup  42416  limclner  42734  fourierdlem51  43240  hoidmvle  43680  smfmullem3  43866