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
s => r is valid by A2, Th50;
then A3: s => r in TAUT by CQC_THE1:def 11;
q => p is valid by A1, Th50;
then q => p in TAUT by CQC_THE1:def 11;
then (q '&' s) => (p '&' r) in TAUT by A3, PROCAL_1:56;
then A4: (q '&' s) => (p '&' r) is valid by CQC_THE1:def 11;
r => s is valid by A2, Th50;
then A5: r => s in TAUT by CQC_THE1:def 11;
p => q is valid by A1, Th50;
then p => q in TAUT by CQC_THE1:def 11;
then (p '&' r) => (q '&' s) in TAUT by A5, PROCAL_1:56;
then (p '&' r) => (q '&' s) is valid by CQC_THE1:def 11;
hence p '&' r <==> q '&' s by A4, Th50; :: thesis: verum