let p, q, r, s be Element of CQC-WFF ; :: thesis: ( p |-| q & r |-| s implies p '&' r |- q '&' s )
assume that
A1: p |-| q and
A2: r |-| s ; :: thesis: p '&' r |- q '&' s
p |- q by A1, Def5;
then {p} |- q by Def1;
then A3: {p,r} |- q by Th4, ZFMISC_1:12;
r |- s by A2, Def5;
then {r} |- s by Def1;
then {p,r} |- s by Th4, ZFMISC_1:12;
then {p,r} |- q '&' s by A3, Lm2;
then A4: {p,r} |- {(q '&' s)} by Th10;
{p,r} |-| {(p '&' r)} by Th31;
then {(p '&' r)} |- {p,r} by Th18;
then {(p '&' r)} |- {(q '&' s)} by A4, Th9;
hence p '&' r |- q '&' s by Th11; :: thesis: verum