theorem :: PROCAL_1:29

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A