Theorem simp-6l 798

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ghmcmn  19892  ustuqtop2  24360  ustuqtop4  24362  cnheibor  25075  miriso  28901  f1otrg  29129  txomap  34141  pstmxmet  34204  omssubadd  34607  signstfvneq0  34876  iunconnlem2  45508  suplesup  45913  limcleqr  46216  0ellimcdiv  46221  limclner  46223  fourierdlem51  46729  smflimlem2  47344  upfval  49805