Metamath Proof Explorer

Theorem dfifp5

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

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

Step	Hyp	Ref	Expression
1		dfifp2	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$
2		imor	$⊢ (φ \to ψ) \leftrightarrow (\neg φ \lor ψ)$
3	2	anbi1i	$⊢ ((φ \to ψ) \land (\neg φ \to χ)) \leftrightarrow ((\neg φ \lor ψ) \land (\neg φ \to χ))$
4	1 3	bitri	$⊢ if- (φ, ψ, χ) \leftrightarrow ((\neg φ \lor ψ) \land (\neg φ \to χ))$