Theorem simp-6l 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-6l	⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

Proof of Theorem simp-6l

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad6antr 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 207  df-an 396

This theorem is referenced by:  ghmcmn  19849  ustuqtop2  24251  ustuqtop4  24253  cnheibor  24987  miriso  28678  f1otrg  28879  txomap  33833  pstmxmet  33896  omssubadd  34302  signstfvneq0  34587  iunconnlem2  44955  suplesup  45350  limcleqr  45659  0ellimcdiv  45664  limclner  45666  fourierdlem51  46172  smflimlem2  46787  upfval  48933