theorem :: XBOOLEAN:27

for p, q being boolean object holds p => (p <=> q) = p => (p => q)