Theorem simp-6l 799

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad6antr 749	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ghmcmn  20078  ustuqtop2  24594  ustuqtop4  24596  cnheibor  25309  miriso  29175  f1otrg  29481  txomap  34549  pstmxmet  34612  omssubadd  35015  signstfvneq0  35284  iunconnlem2  46119  suplesup  46566  limcleqr  46869  0ellimcdiv  46874  limclner  46876  fourierdlem51  47382  smflimlem2  47997  upfval  50507