Theorem bianfi

Description: A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 26-Nov-2012)

	Ref	Expression
Hypothesis	bianfi.1	⊢ ¬ 𝜑
Assertion	bianfi	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		bianfi.1	⊢ ¬ 𝜑
2	1	intnan	⊢ ¬ ( 𝜓 ∧ 𝜑 )
3	1 2	2false	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜑 ) )