Theorem wl-ifp-ncond2

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-ncond2	$$⊢\neg \chi \to \left(if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\phi \wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-ifp-ncond1	$$⊢\neg \chi \to \left(if-\left(\neg \phi ,\chi ,\psi \right)\leftrightarrow \left(\neg \neg \phi \wedge \psi \right)\right)$$
2		ifpn	$$⊢if-\left(\phi ,\psi ,\chi \right)\leftrightarrow if-\left(\neg \phi ,\chi ,\psi \right)$$
3		notnotb	$$⊢\phi \leftrightarrow \neg \neg \phi$$
4	3	anbi1i	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \left(\neg \neg \phi \wedge \psi \right)$$
5	1 2 4	3bitr4g	$$⊢\neg \chi \to \left(if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\phi \wedge \psi \right)\right)$$