ifpim23g

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

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

Proof

Step	Hyp	Ref	Expression
1		ifpidg	$⊢ ((φ \to ψ) \leftrightarrow if- (χ, ψ, \neg φ)) \leftrightarrow ((((χ \land ψ) \to (φ \to ψ)) \land ((χ \land (φ \to ψ)) \to ψ)) \land ((\neg φ \to (χ \lor (φ \to ψ))) \land ((φ \to ψ) \to (χ \lor \neg φ))))$
2		dfor2	$⊢ (φ \lor ψ) \leftrightarrow ((φ \to ψ) \to ψ)$
3	2	imbi2i	$⊢ (χ \to (φ \lor ψ)) \leftrightarrow (χ \to ((φ \to ψ) \to ψ))$
4		impexp	$⊢ ((χ \land (φ \to ψ)) \to ψ) \leftrightarrow (χ \to ((φ \to ψ) \to ψ))$
5		ax-1	$⊢ ψ \to (φ \to ψ)$
6	5	adantl	$⊢ (χ \land ψ) \to (φ \to ψ)$
7	6	biantrur	$⊢ ((χ \land (φ \to ψ)) \to ψ) \leftrightarrow (((χ \land ψ) \to (φ \to ψ)) \land ((χ \land (φ \to ψ)) \to ψ))$
8	3 4 7	3bitr2i	$⊢ (χ \to (φ \lor ψ)) \leftrightarrow (((χ \land ψ) \to (φ \to ψ)) \land ((χ \land (φ \to ψ)) \to ψ))$
9		impexp	$⊢ ((φ \land ψ) \to χ) \leftrightarrow (φ \to (ψ \to χ))$
10		imdi	$⊢ (φ \to (ψ \to χ)) \leftrightarrow ((φ \to ψ) \to (φ \to χ))$
11		imor	$⊢ (φ \to χ) \leftrightarrow (\neg φ \lor χ)$
12		orcom	$⊢ (\neg φ \lor χ) \leftrightarrow (χ \lor \neg φ)$
13	11 12	bitri	$⊢ (φ \to χ) \leftrightarrow (χ \lor \neg φ)$
14	13	imbi2i	$⊢ ((φ \to ψ) \to (φ \to χ)) \leftrightarrow ((φ \to ψ) \to (χ \lor \neg φ))$
15	10 14	bitri	$⊢ (φ \to (ψ \to χ)) \leftrightarrow ((φ \to ψ) \to (χ \lor \neg φ))$
16	9 15	bitri	$⊢ ((φ \land ψ) \to χ) \leftrightarrow ((φ \to ψ) \to (χ \lor \neg φ))$
17		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
18	17	olcd	$⊢ \neg φ \to (χ \lor (φ \to ψ))$
19	18	biantrur	$⊢ ((φ \to ψ) \to (χ \lor \neg φ)) \leftrightarrow ((\neg φ \to (χ \lor (φ \to ψ))) \land ((φ \to ψ) \to (χ \lor \neg φ)))$
20	16 19	bitri	$⊢ ((φ \land ψ) \to χ) \leftrightarrow ((\neg φ \to (χ \lor (φ \to ψ))) \land ((φ \to ψ) \to (χ \lor \neg φ)))$
21	8 20	anbi12i	$⊢ ((χ \to (φ \lor ψ)) \land ((φ \land ψ) \to χ)) \leftrightarrow ((((χ \land ψ) \to (φ \to ψ)) \land ((χ \land (φ \to ψ)) \to ψ)) \land ((\neg φ \to (χ \lor (φ \to ψ))) \land ((φ \to ψ) \to (χ \lor \neg φ))))$
22		ancom	$⊢ ((χ \to (φ \lor ψ)) \land ((φ \land ψ) \to χ)) \leftrightarrow (((φ \land ψ) \to χ) \land (χ \to (φ \lor ψ)))$
23	1 21 22	3bitr2i	$⊢ ((φ \to ψ) \leftrightarrow if- (χ, ψ, \neg φ)) \leftrightarrow (((φ \land ψ) \to χ) \land (χ \to (φ \lor ψ)))$

Metamath Proof Explorer

Theorem ifpim23g

Proof