dfifp6

Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)

		Ref	Expression
	Assertion	dfifp6	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor \neg (χ \to φ))$

Step	Hyp	Ref	Expression
1		df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
2		ancom	$⊢ (\neg φ \land χ) \leftrightarrow (χ \land \neg φ)$
3		annim	$⊢ (χ \land \neg φ) \leftrightarrow \neg (χ \to φ)$
4	2 3	bitri	$⊢ (\neg φ \land χ) \leftrightarrow \neg (χ \to φ)$
5	4	orbi2i	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \land ψ) \lor \neg (χ \to φ))$
6	1 5	bitri	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor \neg (χ \to φ))$

Metamath Proof Explorer