ifpnot23

Description: Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020)

		Ref	Expression
	Assertion	ifpnot23	$⊢ \neg if- (φ, ψ, χ) \leftrightarrow if- (φ, \neg ψ, \neg χ)$

Step	Hyp	Ref	Expression
1		ianor	$⊢ \neg (φ \land ψ) \leftrightarrow (\neg φ \lor \neg ψ)$
2		pm4.55	$⊢ \neg (\neg φ \land χ) \leftrightarrow (φ \lor \neg χ)$
3	1 2	anbi12i	$⊢ (\neg (φ \land ψ) \land \neg (\neg φ \land χ)) \leftrightarrow ((\neg φ \lor \neg ψ) \land (φ \lor \neg χ))$
4		ioran	$⊢ \neg ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow (\neg (φ \land ψ) \land \neg (\neg φ \land χ))$
5		dfifp4	$⊢ if- (φ, \neg ψ, \neg χ) \leftrightarrow ((\neg φ \lor \neg ψ) \land (φ \lor \neg χ))$
6	3 4 5	3bitr4i	$⊢ \neg ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow if- (φ, \neg ψ, \neg χ)$
7		df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
8	6 7	xchnxbir	$⊢ \neg if- (φ, ψ, χ) \leftrightarrow if- (φ, \neg ψ, \neg χ)$

Metamath Proof Explorer