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