environ
    given x being PERSON;
begin

== The proof version

    ( (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x] ) implies R[x]
    proof         == Rule: II
        assume A: (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x];
               1: P[x] by A;                == CE
               2: P[x] implies Q[x] by A;   == CE
               3: Q[x] by 1, 2;             == IE
               4: Q[x] implies R[x] by A;   == CE
        thus R[x] by 3,4;                   == IE
    end;

== The now version

 1: now
        assume A: (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x];
               1: P[x] by A;                == CE
               2: P[x] implies Q[x] by A;   == CE
               3: Q[x] by 1, 2;             == IE
               4: Q[x] implies R[x] by A;   == CE
        thus R[x] by 3,4;                   == IE
    end;

    ( (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x] ) implies R[x]
                                         by 1;     == II