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
'not' r <==> 'not' s by A2, Lm5;
then p '&' ('not' r) <==> q '&' ('not' s) by A1, Th54;
then A3: 'not' (p '&' ('not' r)) <==> 'not' (q '&' ('not' s)) by Lm5;
p => r = 'not' (p '&' ('not' r)) by QC_LANG2:def 2;
hence p => r <==> q => s by A3, QC_LANG2:def 2; :: thesis: verum