# 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 ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\chi }↔{\psi }\right)↔\left({\phi }↔{\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 bicom ${⊢}\left({\phi }↔{\psi }\right)↔\left({\psi }↔{\phi }\right)$
2 1 bibi1i ${⊢}\left(\left({\phi }↔{\psi }\right)↔{\chi }\right)↔\left(\left({\psi }↔{\phi }\right)↔{\chi }\right)$
3 biass ${⊢}\left(\left({\psi }↔{\phi }\right)↔{\chi }\right)↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)$
4 2 3 bitri ${⊢}\left(\left({\phi }↔{\psi }\right)↔{\chi }\right)↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)$
5 biass ${⊢}\left(\left(\left({\phi }↔{\psi }\right)↔{\chi }\right)↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)\right)↔\left(\left({\phi }↔{\psi }\right)↔\left({\chi }↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)\right)\right)$
6 4 5 mpbi ${⊢}\left({\phi }↔{\psi }\right)↔\left({\chi }↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)\right)$
7 biass ${⊢}\left(\left({\chi }↔{\psi }\right)↔\left({\phi }↔{\chi }\right)\right)↔\left({\chi }↔\left({\psi }↔\left({\phi }↔{\chi }\right)\right)\right)$
8 6 7 bitr4i ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\chi }↔{\psi }\right)↔\left({\phi }↔{\chi }\right)\right)$