ifpid2g

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

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

Step	Hyp	Ref	Expression
1		ifpidg	$⊢ (ψ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((((φ \land ψ) \to ψ) \land ((φ \land ψ) \to ψ)) \land ((χ \to (φ \lor ψ)) \land (ψ \to (φ \lor χ))))$
2		simpr	$⊢ (φ \land ψ) \to ψ$
3	2 2	pm3.2i	$⊢ (((φ \land ψ) \to ψ) \land ((φ \land ψ) \to ψ))$
4	3	biantrur	$⊢ ((χ \to (φ \lor ψ)) \land (ψ \to (φ \lor χ))) \leftrightarrow ((((φ \land ψ) \to ψ) \land ((φ \land ψ) \to ψ)) \land ((χ \to (φ \lor ψ)) \land (ψ \to (φ \lor χ))))$
5		ancom	$⊢ ((χ \to (φ \lor ψ)) \land (ψ \to (φ \lor χ))) \leftrightarrow ((ψ \to (φ \lor χ)) \land (χ \to (φ \lor ψ)))$
6	1 4 5	3bitr2i	$⊢ (ψ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((ψ \to (φ \lor χ)) \land (χ \to (φ \lor ψ)))$

Metamath Proof Explorer