let p, q, r be Element of MC-wff ; :: thesis: |-_IPC (p => (q 'or' (p => r))) => (p => (q 'or' r))
set V = q 'or' r;
A1: {r} |-_IPC q 'or' r by Th121;
{r} c= {p} \/ {r} by XBOOLE_1:7;
then A3: {p} \/ {r} |-_IPC q 'or' r by A1, Th66;
A4: {p} |-_IPC p by Th65;
then A5: {p} \/ {(p => r)} |-_IPC q 'or' r by A3, Th119;
A7: {q} |-_IPC q 'or' r by Th120;
{q} c= {p} \/ {q} by XBOOLE_1:7;
then {p} \/ {q} |-_IPC q 'or' r by A7, Th66;
then {p} \/ {(q 'or' (p => r))} |-_IPC q 'or' r by A5, Th123;
then {p} \/ {(p => (q 'or' (p => r)))} |-_IPC q 'or' r by A4, Th119;
then {(p => (q 'or' (p => r)))} |-_IPC p => (q 'or' r) by Th53;
hence |-_IPC (p => (q 'or' (p => r))) => (p => (q 'or' r)) by Th54; :: thesis: verum