ifpid1g

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

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

Step	Hyp	Ref	Expression
1		ifpidg	$⊢ (φ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ)) \land ((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ))))$
2		ancom	$⊢ ((((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ)) \land ((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ)))) \leftrightarrow (((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ))) \land (((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ)))$
3		pm4.25	$⊢ φ \leftrightarrow (φ \lor φ)$
4	3	imbi2i	$⊢ (χ \to φ) \leftrightarrow (χ \to (φ \lor φ))$
5		orc	$⊢ φ \to (φ \lor χ)$
6	5	biantru	$⊢ (χ \to (φ \lor φ)) \leftrightarrow ((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ)))$
7	4 6	bitr2i	$⊢ ((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ))) \leftrightarrow (χ \to φ)$
8		pm4.24	$⊢ φ \leftrightarrow (φ \land φ)$
9	8	imbi1i	$⊢ (φ \to ψ) \leftrightarrow ((φ \land φ) \to ψ)$
10		simpl	$⊢ (φ \land ψ) \to φ$
11	10	biantrur	$⊢ ((φ \land φ) \to ψ) \leftrightarrow (((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ))$
12	9 11	bitr2i	$⊢ (((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ)) \leftrightarrow (φ \to ψ)$
13	7 12	anbi12i	$⊢ (((χ \to (φ \lor φ)) \land (φ \to (φ \lor χ))) \land (((φ \land ψ) \to φ) \land ((φ \land φ) \to ψ))) \leftrightarrow ((χ \to φ) \land (φ \to ψ))$
14	1 2 13	3bitri	$⊢ (φ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((χ \to φ) \land (φ \to ψ))$

Metamath Proof Explorer