let p, q, r, s be Element of CQC-WFF ; :: thesis: ( p <==> q & r <==> s implies p 'or' r <==> q 'or' s )
assume that
A1: p <==> q and
A2: r <==> s ; :: thesis: p 'or' r <==> q 'or' 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 'or' r) => (q 'or' s) in TAUT & (q 'or' s) => (p 'or' r) in TAUT ) by A3, PROCAL_1:57;
then ( (p 'or' r) => (q 'or' s) is valid & (q 'or' s) => (p 'or' r) is valid ) by CQC_THE1:def 11;
hence p 'or' r <==> q 'or' s by Th50; :: thesis: verum