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
A3: q '&' s |- p '&' r by A1, A2, Lm4;
p '&' r |- q '&' s by A1, A2, Lm4;
hence p '&' r |-| q '&' s by A3, Def5; :: thesis: verum