Theorem simp-6r 786

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  catass  16959  mhmmnd  18223  scmatscm  21124  cfilucfil  23171  2sqmo  26015  istrkgb  26243  istrkge  26245  tgbtwnconn1  26363  legso  26387  footexALT  26506  opphl  26542  trgcopy  26592  dfcgra2  26618  cgrg3col4  26641  f1otrg  26659  cyc3genpm  30796  cyc3conja  30801  ssmxidllem  30980  pstmxmet  31139  signstfvneq0  31844  afsval  31944  mblfinlem3  34933  mblfinlem4  34934  dffltz  39278  iunconnlem2  41276  suplesup  41614  limclner  41939  fourierdlem51  42449  hoidmvle  42889  smfmullem3  43075