theorem :: XBOOLEAN:133

for p, q, r, s being boolean object st p <=> q = TRUE & r <=> s = TRUE holds
(p => r) <=> (q => s) = TRUE