Metamath Proof Explorer

Theorem biluk

Description: Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed.,Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005)

Ref Expression
Assertion biluk ⊢φ↔ψ↔χ↔ψ↔φ↔χ

Proof

Step Hyp Ref Expression
1 bicom ⊢φ↔ψ↔ψ↔φ
2 1 bibi1i ⊢φ↔ψ↔χ↔ψ↔φ↔χ
3 biass ⊢ψ↔φ↔χ↔ψ↔φ↔χ
4 2 3 bitri ⊢φ↔ψ↔χ↔ψ↔φ↔χ
5 biass ⊢φ↔ψ↔χ↔ψ↔φ↔χ↔φ↔ψ↔χ↔ψ↔φ↔χ
6 4 5 mpbi ⊢φ↔ψ↔χ↔ψ↔φ↔χ
7 biass ⊢χ↔ψ↔φ↔χ↔χ↔ψ↔φ↔χ
8 6 7 bitr4i ⊢φ↔ψ↔χ↔ψ↔φ↔χ