Theorem biass 744

Description: Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseer.ist.psu.edu/lifschitz98calculational.html. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (The proof was shortened by Juha Arpiainen, 19-Jan-2006.)

Assertion

Ref	Expression
biass	|- (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch)))

Proof of Theorem biass

Step	Hyp	Ref	Expression
1		pm5.501 595	. . . 4 |- (ph -> (ps <-> (ph <-> ps)))
2	1	bibi1d 619	. . 3 |- (ph -> ((ps <-> ch) <-> ((ph <-> ps) <-> ch)))
3		pm5.501 595	. . 3 |- (ph -> ((ps <-> ch) <-> (ph <-> (ps <-> ch))))
4	2, 3	bitr3d 530	. 2 |- (ph -> (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch))))
5		nbbn 661	. . . 4 |- ((-. ps <-> ch) <-> -. (ps <-> ch))
6	5	a1i 8	. . 3 |- (-. ph -> ((-. ps <-> ch) <-> -. (ps <-> ch)))
7		nbn2 721	. . . 4 |- (-. ph -> (-. ps <-> (ph <-> ps)))
8	7	bibi1d 619	. . 3 |- (-. ph -> ((-. ps <-> ch) <-> ((ph <-> ps) <-> ch)))
9		nbn2 721	. . 3 |- (-. ph -> (-. (ps <-> ch) <-> (ph <-> (ps <-> ch))))
10	6, 8, 9	3bitr3d 548	. 2 |- (-. ph -> (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch))))
11	4, 10	pm2.61i 126	1 |- (((ph <-> ps) <-> ch) <-> (ph <-> (ps <-> ch)))

Syntax hints:  -. wn 2   <-> wb 146

This theorem is referenced by:  biluk 745

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain