let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D holds PP_and ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_or (p,q)),r)
let p, q, r be PartialPredicate of D; :: thesis: PP_and ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_or (p,q)),r)
thus PP_and ((PP_imp (p,r)),(PP_imp (q,r))) = PP_not (PP_or ((PP_and (p,(PP_not r))),(PP_and (q,(PP_not r)))))
.= PP_not (PP_and ((PP_not r),(PP_or (p,q)))) by Th30
.= PP_imp ((PP_or (p,q)),r) ; :: thesis: verum