Theorem bianfd

Description: A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995) (Proof shortened by Wolf Lammen, 5-Nov-2013)

	Ref	Expression
Hypothesis	bianfd.1	⊢ ( 𝜑 → ¬ 𝜓 )
Assertion	bianfd	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜓 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bianfd.1	⊢ ( 𝜑 → ¬ 𝜓 )
2	1	intnanrd	⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) )
3	1 2	2falsed	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜓 ∧ 𝜒 ) ) )