theorem :: PARTPR_1:27

for D being non empty set
for p, q, r being PartialPredicate of D holds PP_and ((PP_and (p,q)),(PP_and (p,r))) = PP_and ((PP_and (p,q)),r) by Th15;