Metamath Proof Explorer

Theorem dfifp7

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

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

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