Theorem biass 743

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	⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))

Proof of Theorem biass

Step	Hyp	Ref	Expression
1		pm5.501 594	. . . 4 ⊢ (φ → (ψ ↔ (φ ↔ ψ)))
2	1	bibi1d 618	. . 3 ⊢ (φ → ((ψ ↔ χ) ↔ ((φ ↔ ψ) ↔ χ)))
3		pm5.501 594	. . 3 ⊢ (φ → ((ψ ↔ χ) ↔ (φ ↔ (ψ ↔ χ))))
4	2, 3	bitr3d 529	. 2 ⊢ (φ → (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ))))
5		nbbn 660	. . . 4 ⊢ ((¬ ψ ↔ χ) ↔ ¬ (ψ ↔ χ))
6	5	a1i 8	. . 3 ⊢ (¬ φ → ((¬ ψ ↔ χ) ↔ ¬ (ψ ↔ χ)))
7		nbn2 720	. . . 4 ⊢ (¬ φ → (¬ ψ ↔ (φ ↔ ψ)))
8	7	bibi1d 618	. . 3 ⊢ (¬ φ → ((¬ ψ ↔ χ) ↔ ((φ ↔ ψ) ↔ χ)))
9		nbn2 720	. . 3 ⊢ (¬ φ → (¬ (ψ ↔ χ) ↔ (φ ↔ (ψ ↔ χ))))
10	6, 8, 9	3bitr3d 547	. 2 ⊢ (¬ φ → (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ))))
11	4, 10	pm2.61i 126	1 ⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))

Syntax hints:  ¬ wn 2   ↔ wb 146

This theorem is referenced by:  biluk 744

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