theorem :: PARTPR_1:42

for D being non empty set
for p, q, r being PartialPredicate of D holds PP_or ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_and (p,q)),r)