let D be non empty set ; :: thesis: 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)
let p, q, r be PartialPredicate of D; :: thesis: PP_or ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_and (p,q)),r)
PP_or ((PP_or (r,(PP_not p))),(PP_or (r,(PP_not q)))) = PP_or ((PP_or (r,(PP_not p))),(PP_not q)) by Th15;
hence PP_or ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_and (p,q)),r) by Th14; :: thesis: verum