let A be QC-alphabet ; :: thesis: for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |- q '&' s
let p, q, r, s be Element of CQC-WFF A; :: thesis: ( p |-| q & r |-| s implies p '&' r |- q '&' s )
assume that
A1: p |-| q and
A2: r |-| s ; :: thesis: p '&' r |- q '&' s
r |- s by A2;
then {r} |- s ;
then A3: {p,r} |- s by Th4, ZFMISC_1:7;
{p,r} |-| {(p '&' r)} by Th31;
then A4: {(p '&' r)} |- {p,r} by Th18;
p |- q by A1;
then {p} |- q ;
then {p,r} |- q by Th4, ZFMISC_1:7;
then {p,r} |- q '&' s by A3, Lm2;
then {p,r} |- {(q '&' s)} by Th10;
then {(p '&' r)} |- {(q '&' s)} by A4, Th9;
hence p '&' r |- q '&' s by Th11; :: thesis: verum