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	|- ( ( ph <-> ps ) <-> ( ( ch <-> ps ) <-> ( ph <-> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		bicom	|- ( ( ph <-> ps ) <-> ( ps <-> ph ) )
2	1	bibi1i	|- ( ( ( ph <-> ps ) <-> ch ) <-> ( ( ps <-> ph ) <-> ch ) )
3		biass	|- ( ( ( ps <-> ph ) <-> ch ) <-> ( ps <-> ( ph <-> ch ) ) )
4	2 3	bitri	|- ( ( ( ph <-> ps ) <-> ch ) <-> ( ps <-> ( ph <-> ch ) ) )
5		biass	|- ( ( ( ( ph <-> ps ) <-> ch ) <-> ( ps <-> ( ph <-> ch ) ) ) <-> ( ( ph <-> ps ) <-> ( ch <-> ( ps <-> ( ph <-> ch ) ) ) ) )
6	4 5	mpbi	|- ( ( ph <-> ps ) <-> ( ch <-> ( ps <-> ( ph <-> ch ) ) ) )
7		biass	|- ( ( ( ch <-> ps ) <-> ( ph <-> ch ) ) <-> ( ch <-> ( ps <-> ( ph <-> ch ) ) ) )
8	6 7	bitr4i	|- ( ( ph <-> ps ) <-> ( ( ch <-> ps ) <-> ( ph <-> ch ) ) )