Theorem anabsan

Description: Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996)

	Ref	Expression
Hypothesis	anabsan.1	⊢ ( ( ( 𝜑 ∧ 𝜑 ) ∧ 𝜓 ) → 𝜒 )
Assertion	anabsan	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		anabsan.1	⊢ ( ( ( 𝜑 ∧ 𝜑 ) ∧ 𝜓 ) → 𝜒 )
2		pm4.24	⊢ ( 𝜑 ↔ ( 𝜑 ∧ 𝜑 ) )
3	2 1	sylanb	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )