let A be QC-alphabet ; :: thesis: for p, q, r, s being Element of CQC-WFF A st p <==> q & r <==> s holds
p 'or' r <==> q 'or' s
let p, q, r, s be Element of CQC-WFF A; :: 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
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 'or' s) => (p 'or' r) in TAUT A by A3, PROCAL_1:57;
then A4: (q 'or' s) => (p 'or' 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 'or' r) => (q 'or' s) in TAUT A by A5, PROCAL_1:57;
then (p 'or' r) => (q 'or' s) is valid by CQC_THE1:def 10;
hence p 'or' r <==> q 'or' s by A4, Th50; :: thesis: verum