Per definizione di regola derivabile, occorre  dimostrare:
1. {R = R', (PR) = (QR)}  |- CL1 (PR)=(QR')
2. {R = R', (RP) = (RQ)}  |- CL1 (RP)=(R'Q)

Per la  1. forniamo la seguente deduzione in CL1:

i) R = R'        (ipotesi)
ii)(PR)=(QR)     (ipotesi)
iii)Q = Q        [Assioma di Riflessivita')
iv)(QR) = (QR')  CONGR(iii, i)
v)(PR) = (QR')   TRANS(ii, iv)

Per la 2. forniamo la seguente deduzione in CL1:


i) R = R'         (ipotesi)
ii)(RP)=(RQ)      (ipotesi)
iii)Q = Q         (Assioma di Riflessivita') 
iv)(RQ) = (RQ')   CONGR(i, iii)
v)(RP) = (R'Q)    TRANS(ii, iv)