Theorem simp-6r 785

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 734	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  17637  mhmmnd  18990  scmatscm  22335  cfilucfil  24388  2sqmo  27284  tgbtwnconn1  28260  legso  28284  footexALT  28403  opphl  28439  trgcopy  28489  dfcgra2  28515  cgrg3col4  28538  f1otrg  28556  2ndresdju  32308  cyc3genpm  32748  cyc3conja  32753  rhmquskerlem  32984  rhmimaidl  32991  mxidlirredi  33028  ssmxidllem  33030  r1plmhm  33122  r1pquslmic  33123  pstmxmet  33342  signstfvneq0  34048  afsval  34148  mblfinlem3  36993  mblfinlem4  36994  dffltz  41841  iunconnlem2  44161  suplesup  44510  limclner  44828  fourierdlem51  45334  hoidmvle  45777  smfmullem3  45970