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