let A be QC-alphabet ; 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; ( p |-| q & r |-| s implies p '&' r |- q '&' s )
assume that
A1:
p |-| q
and
A2:
r |-| s
; 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; verum