Metamath Proof Explorer

Theorem ifpid3g

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

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

Step	Hyp	Ref	Expression
1		olc	$⊢ χ \to (φ \lor χ)$
2	1 1	pm3.2i	$⊢ ((χ \to (φ \lor χ)) \land (χ \to (φ \lor χ)))$
3		ifpidg	$⊢ (χ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((((φ \land ψ) \to χ) \land ((φ \land χ) \to ψ)) \land ((χ \to (φ \lor χ)) \land (χ \to (φ \lor χ))))$
4	2 3	mpbiran2	$⊢ (χ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow (((φ \land ψ) \to χ) \land ((φ \land χ) \to ψ))$