ifpidg

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

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

Proof

Step	Hyp	Ref	Expression
1		dfifp4	$⊢ if- (φ, ψ, χ) \leftrightarrow ((\neg φ \lor ψ) \land (φ \lor χ))$
2	1	bibi2i	$⊢ (θ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow (θ \leftrightarrow ((\neg φ \lor ψ) \land (φ \lor χ)))$
3		dfbi2	$⊢ (θ \leftrightarrow ((\neg φ \lor ψ) \land (φ \lor χ))) \leftrightarrow ((θ \to ((\neg φ \lor ψ) \land (φ \lor χ))) \land (((\neg φ \lor ψ) \land (φ \lor χ)) \to θ))$
4		imor	$⊢ (θ \to ((\neg φ \lor ψ) \land (φ \lor χ))) \leftrightarrow (\neg θ \lor ((\neg φ \lor ψ) \land (φ \lor χ)))$
5		ordi	$⊢ (\neg θ \lor ((\neg φ \lor ψ) \land (φ \lor χ))) \leftrightarrow ((\neg θ \lor (\neg φ \lor ψ)) \land (\neg θ \lor (φ \lor χ)))$
6		ancomst	$⊢ ((φ \land θ) \to ψ) \leftrightarrow ((θ \land φ) \to ψ)$
7		impexp	$⊢ ((θ \land φ) \to ψ) \leftrightarrow (θ \to (φ \to ψ))$
8		imor	$⊢ (φ \to ψ) \leftrightarrow (\neg φ \lor ψ)$
9	8	imbi2i	$⊢ (θ \to (φ \to ψ)) \leftrightarrow (θ \to (\neg φ \lor ψ))$
10		imor	$⊢ (θ \to (\neg φ \lor ψ)) \leftrightarrow (\neg θ \lor (\neg φ \lor ψ))$
11	9 10	bitri	$⊢ (θ \to (φ \to ψ)) \leftrightarrow (\neg θ \lor (\neg φ \lor ψ))$
12	6 7 11	3bitrri	$⊢ (\neg θ \lor (\neg φ \lor ψ)) \leftrightarrow ((φ \land θ) \to ψ)$
13		imor	$⊢ (θ \to (φ \lor χ)) \leftrightarrow (\neg θ \lor (φ \lor χ))$
14	13	bicomi	$⊢ (\neg θ \lor (φ \lor χ)) \leftrightarrow (θ \to (φ \lor χ))$
15	12 14	anbi12i	$⊢ ((\neg θ \lor (\neg φ \lor ψ)) \land (\neg θ \lor (φ \lor χ))) \leftrightarrow (((φ \land θ) \to ψ) \land (θ \to (φ \lor χ)))$
16	4 5 15	3bitri	$⊢ (θ \to ((\neg φ \lor ψ) \land (φ \lor χ))) \leftrightarrow (((φ \land θ) \to ψ) \land (θ \to (φ \lor χ)))$
17	8	bicomi	$⊢ (\neg φ \lor ψ) \leftrightarrow (φ \to ψ)$
18		df-or	$⊢ (φ \lor χ) \leftrightarrow (\neg φ \to χ)$
19	17 18	anbi12i	$⊢ ((\neg φ \lor ψ) \land (φ \lor χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$
20		cases2	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$
21	20	bicomi	$⊢ ((φ \to ψ) \land (\neg φ \to χ)) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
22	19 21	bitri	$⊢ ((\neg φ \lor ψ) \land (φ \lor χ)) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
23	22	imbi1i	$⊢ (((\neg φ \lor ψ) \land (φ \lor χ)) \to θ) \leftrightarrow (((φ \land ψ) \lor (\neg φ \land χ)) \to θ)$
24		jaob	$⊢ (((φ \land ψ) \lor (\neg φ \land χ)) \to θ) \leftrightarrow (((φ \land ψ) \to θ) \land ((\neg φ \land χ) \to θ))$
25		ancomst	$⊢ ((\neg φ \land χ) \to θ) \leftrightarrow ((χ \land \neg φ) \to θ)$
26		pm5.6	$⊢ ((χ \land \neg φ) \to θ) \leftrightarrow (χ \to (φ \lor θ))$
27	25 26	bitri	$⊢ ((\neg φ \land χ) \to θ) \leftrightarrow (χ \to (φ \lor θ))$
28	27	anbi2i	$⊢ (((φ \land ψ) \to θ) \land ((\neg φ \land χ) \to θ)) \leftrightarrow (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ)))$
29	23 24 28	3bitri	$⊢ (((\neg φ \lor ψ) \land (φ \lor χ)) \to θ) \leftrightarrow (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ)))$
30	16 29	anbi12i	$⊢ ((θ \to ((\neg φ \lor ψ) \land (φ \lor χ))) \land (((\neg φ \lor ψ) \land (φ \lor χ)) \to θ)) \leftrightarrow ((((φ \land θ) \to ψ) \land (θ \to (φ \lor χ))) \land (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ))))$
31	3 30	bitri	$⊢ (θ \leftrightarrow ((\neg φ \lor ψ) \land (φ \lor χ))) \leftrightarrow ((((φ \land θ) \to ψ) \land (θ \to (φ \lor χ))) \land (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ))))$
32		ancom	$⊢ ((((φ \land θ) \to ψ) \land (θ \to (φ \lor χ))) \land (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ)))) \leftrightarrow ((((φ \land ψ) \to θ) \land (χ \to (φ \lor θ))) \land (((φ \land θ) \to ψ) \land (θ \to (φ \lor χ))))$
33		an4	$⊢ ((((φ \land ψ) \to θ) \land (χ \to (φ \lor θ))) \land (((φ \land θ) \to ψ) \land (θ \to (φ \lor χ)))) \leftrightarrow ((((φ \land ψ) \to θ) \land ((φ \land θ) \to ψ)) \land ((χ \to (φ \lor θ)) \land (θ \to (φ \lor χ))))$
34	32 33	bitri	$⊢ ((((φ \land θ) \to ψ) \land (θ \to (φ \lor χ))) \land (((φ \land ψ) \to θ) \land (χ \to (φ \lor θ)))) \leftrightarrow ((((φ \land ψ) \to θ) \land ((φ \land θ) \to ψ)) \land ((χ \to (φ \lor θ)) \land (θ \to (φ \lor χ))))$
35	2 31 34	3bitri	$⊢ (θ \leftrightarrow if- (φ, ψ, χ)) \leftrightarrow ((((φ \land ψ) \to θ) \land ((φ \land θ) \to ψ)) \land ((χ \to (φ \lor θ)) \land (θ \to (φ \lor χ))))$

Metamath Proof Explorer

Theorem ifpidg

Proof