Theorem biass 511

Description: Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.lcs.mit.edu/lifschitz98calculational.html. Noted by Jan Lukasiewicz c. 1923.

Assertion

Ref	Expression
biass	⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))

Proof of Theorem biass

Step	Hyp	Ref	Expression
1		andi 456	. . . 4 ⊢ ((φ ∧ ((ψ ∧ χ) ∨ (¬ ψ ∧ ¬ χ))) ↔ ((φ ∧ (ψ ∧ χ)) ∨ (φ ∧ (¬ ψ ∧ ¬ χ))))
2		dfbi 499	. . . . 5 ⊢ ((ψ ↔ χ) ↔ ((ψ ∧ χ) ∨ (¬ ψ ∧ ¬ χ)))
3	2	anbi2i 367	. . . 4 ⊢ ((φ ∧ (ψ ↔ χ)) ↔ (φ ∧ ((ψ ∧ χ) ∨ (¬ ψ ∧ ¬ χ))))
4		anass 336	. . . . 5 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
5		anass 336	. . . . 5 ⊢ (((φ ∧ ¬ ψ) ∧ ¬ χ) ↔ (φ ∧ (¬ ψ ∧ ¬ χ)))
6	4, 5	orbi12i 216	. . . 4 ⊢ ((((φ ∧ ψ) ∧ χ) ∨ ((φ ∧ ¬ ψ) ∧ ¬ χ)) ↔ ((φ ∧ (ψ ∧ χ)) ∨ (φ ∧ (¬ ψ ∧ ¬ χ))))
7	1, 3, 6	3bitr4 158	. . 3 ⊢ ((φ ∧ (ψ ↔ χ)) ↔ (((φ ∧ ψ) ∧ χ) ∨ ((φ ∧ ¬ ψ) ∧ ¬ χ)))
8		andi 456	. . . 4 ⊢ ((¬ φ ∧ ((ψ ∧ ¬ χ) ∨ (¬ ψ ∧ χ))) ↔ ((¬ φ ∧ (ψ ∧ ¬ χ)) ∨ (¬ φ ∧ (¬ ψ ∧ χ))))
9		xor 500	. . . . . 6 ⊢ (¬ (ψ ↔ χ) ↔ ((ψ ∧ ¬ χ) ∨ (χ ∧ ¬ ψ)))
10		ancom 333	. . . . . . 7 ⊢ ((χ ∧ ¬ ψ) ↔ (¬ ψ ∧ χ))
11	10	orbi2i 214	. . . . . 6 ⊢ (((ψ ∧ ¬ χ) ∨ (χ ∧ ¬ ψ)) ↔ ((ψ ∧ ¬ χ) ∨ (¬ ψ ∧ χ)))
12	9, 11	bitr 151	. . . . 5 ⊢ (¬ (ψ ↔ χ) ↔ ((ψ ∧ ¬ χ) ∨ (¬ ψ ∧ χ)))
13	12	anbi2i 367	. . . 4 ⊢ ((¬ φ ∧ ¬ (ψ ↔ χ)) ↔ (¬ φ ∧ ((ψ ∧ ¬ χ) ∨ (¬ ψ ∧ χ))))
14		anass 336	. . . . 5 ⊢ (((¬ φ ∧ ψ) ∧ ¬ χ) ↔ (¬ φ ∧ (ψ ∧ ¬ χ)))
15		anass 336	. . . . 5 ⊢ (((¬ φ ∧ ¬ ψ) ∧ χ) ↔ (¬ φ ∧ (¬ ψ ∧ χ)))
16	14, 15	orbi12i 216	. . . 4 ⊢ ((((¬ φ ∧ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)) ↔ ((¬ φ ∧ (ψ ∧ ¬ χ)) ∨ (¬ φ ∧ (¬ ψ ∧ χ))))
17	8, 13, 16	3bitr4 158	. . 3 ⊢ ((¬ φ ∧ ¬ (ψ ↔ χ)) ↔ (((¬ φ ∧ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)))
18	7, 17	orbi12i 216	. 2 ⊢ (((φ ∧ (ψ ↔ χ)) ∨ (¬ φ ∧ ¬ (ψ ↔ χ))) ↔ ((((φ ∧ ψ) ∧ χ) ∨ ((φ ∧ ¬ ψ) ∧ ¬ χ)) ∨ (((¬ φ ∧ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ))))
19		dfbi 499	. 2 ⊢ ((φ ↔ (ψ ↔ χ)) ↔ ((φ ∧ (ψ ↔ χ)) ∨ (¬ φ ∧ ¬ (ψ ↔ χ))))
20		dfbi 499	. . 3 ⊢ (((φ ↔ ψ) ↔ χ) ↔ (((φ ↔ ψ) ∧ χ) ∨ (¬ (φ ↔ ψ) ∧ ¬ χ)))
21		dfbi 499	. . . . . 6 ⊢ ((φ ↔ ψ) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)))
22	21	anbi1i 368	. . . . 5 ⊢ (((φ ↔ ψ) ∧ χ) ↔ (((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ∧ χ))
23		andir 457	. . . . 5 ⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ ¬ ψ)) ∧ χ) ↔ (((φ ∧ ψ) ∧ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)))
24	22, 23	bitr 151	. . . 4 ⊢ (((φ ↔ ψ) ∧ χ) ↔ (((φ ∧ ψ) ∧ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)))
25		xor 500	. . . . . . 7 ⊢ (¬ (φ ↔ ψ) ↔ ((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)))
26		ancom 333	. . . . . . . 8 ⊢ ((ψ ∧ ¬ φ) ↔ (¬ φ ∧ ψ))
27	26	orbi2i 214	. . . . . . 7 ⊢ (((φ ∧ ¬ ψ) ∨ (ψ ∧ ¬ φ)) ↔ ((φ ∧ ¬ ψ) ∨ (¬ φ ∧ ψ)))
28	25, 27	bitr 151	. . . . . 6 ⊢ (¬ (φ ↔ ψ) ↔ ((φ ∧ ¬ ψ) ∨ (¬ φ ∧ ψ)))
29	28	anbi1i 368	. . . . 5 ⊢ ((¬ (φ ↔ ψ) ∧ ¬ χ) ↔ (((φ ∧ ¬ ψ) ∨ (¬ φ ∧ ψ)) ∧ ¬ χ))
30		andir 457	. . . . 5 ⊢ ((((φ ∧ ¬ ψ) ∨ (¬ φ ∧ ψ)) ∧ ¬ χ) ↔ (((φ ∧ ¬ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ψ) ∧ ¬ χ)))
31	29, 30	bitr 151	. . . 4 ⊢ ((¬ (φ ↔ ψ) ∧ ¬ χ) ↔ (((φ ∧ ¬ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ψ) ∧ ¬ χ)))
32	24, 31	orbi12i 216	. . 3 ⊢ ((((φ ↔ ψ) ∧ χ) ∨ (¬ (φ ↔ ψ) ∧ ¬ χ)) ↔ ((((φ ∧ ψ) ∧ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)) ∨ (((φ ∧ ¬ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ψ) ∧ ¬ χ))))
33		or42 221	. . 3 ⊢ (((((φ ∧ ψ) ∧ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ)) ∨ (((φ ∧ ¬ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ψ) ∧ ¬ χ))) ↔ ((((φ ∧ ψ) ∧ χ) ∨ ((φ ∧ ¬ ψ) ∧ ¬ χ)) ∨ (((¬ φ ∧ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ))))
34	20, 32, 33	3bitr 155	. 2 ⊢ (((φ ↔ ψ) ↔ χ) ↔ ((((φ ∧ ψ) ∧ χ) ∨ ((φ ∧ ¬ ψ) ∧ ¬ χ)) ∨ (((¬ φ ∧ ψ) ∧ ¬ χ) ∨ ((¬ φ ∧ ¬ ψ) ∧ χ))))
35	18, 19, 34	3bitr4r 159	1 ⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))

Syntax hints:  ¬ wn 1   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  biluk 512

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org