wl-ifp-ncond1

Description: If one case of an if- condition is false, the other automatically follows. (Contributed by Wolf Lammen, 21-Jul-2024)

		Ref	Expression
	Assertion	wl-ifp-ncond1	$⊢ \neg ψ \to (if- (φ, ψ, χ) \leftrightarrow (\neg φ \land χ))$

Step	Hyp	Ref	Expression
1		df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
2		simpr	$⊢ (φ \land ψ) \to ψ$
3	2	con3i	$⊢ \neg ψ \to \neg (φ \land ψ)$
4		biorf	$⊢ \neg (φ \land ψ) \to ((\neg φ \land χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ)))$
5	3 4	syl	$⊢ \neg ψ \to ((\neg φ \land χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ)))$
6	1 5	bitr4id	$⊢ \neg ψ \to (if- (φ, ψ, χ) \leftrightarrow (\neg φ \land χ))$

Metamath Proof Explorer