let p, q, r be boolean object ; :: thesis: (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE
A1: ( q = FALSE or q = TRUE ) by Def3;
A2: ( p = FALSE or p = TRUE ) by Def3;
( r = FALSE or r = TRUE ) by Def3;
hence (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE by A1, A2; :: thesis: verum