Theorem 3anidm

Description: Idempotent law for conjunction. (Contributed by Peter Mazsa, 17-Oct-2023)

	Ref	Expression
Assertion	3anidm	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝜑 ) ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-3an	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝜑 ) ↔ ( ( 𝜑 ∧ 𝜑 ) ∧ 𝜑 ) )
2		anabs1	⊢ ( ( ( 𝜑 ∧ 𝜑 ) ∧ 𝜑 ) ↔ ( 𝜑 ∧ 𝜑 ) )
3		anidm	⊢ ( ( 𝜑 ∧ 𝜑 ) ↔ 𝜑 )
4	1 2 3	3bitri	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝜑 ) ↔ 𝜑 )