ifpim1

Description: Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020)

		Ref	Expression
	Assertion	ifpim1	$⊢ (φ \to ψ) \leftrightarrow if- (\neg φ, ⊤, ψ)$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2	1	olci	$⊢ (\neg \neg φ \lor ⊤)$
3	2	biantrur	$⊢ (\neg φ \lor ψ) \leftrightarrow ((\neg \neg φ \lor ⊤) \land (\neg φ \lor ψ))$
4		imor	$⊢ (φ \to ψ) \leftrightarrow (\neg φ \lor ψ)$
5		dfifp4	$⊢ if- (\neg φ, ⊤, ψ) \leftrightarrow ((\neg \neg φ \lor ⊤) \land (\neg φ \lor ψ))$
6	3 4 5	3bitr4i	$⊢ (φ \to ψ) \leftrightarrow if- (\neg φ, ⊤, ψ)$

Metamath Proof Explorer