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