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	|- (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch)))

Proof of Theorem biass

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

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