This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 ) ) )