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 396

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 397

This theorem is referenced by:  catass  17634  mhmmnd  18983  scmatscm  22235  cfilucfil  24288  2sqmo  27164  tgbtwnconn1  28081  legso  28105  footexALT  28224  opphl  28260  trgcopy  28310  dfcgra2  28336  cgrg3col4  28359  f1otrg  28377  2ndresdju  32129  cyc3genpm  32569  cyc3conja  32574  rhmquskerlem  32805  rhmimaidl  32812  mxidlirredi  32849  ssmxidllem  32851  r1plmhm  32943  r1pquslmic  32944  pstmxmet  33163  signstfvneq0  33869  afsval  33969  mblfinlem3  36830  mblfinlem4  36831  dffltz  41678  iunconnlem2  43998  suplesup  44348  limclner  44666  fourierdlem51  45172  hoidmvle  45615  smfmullem3  45808