let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st p <==> q holds
All x,p <==> All x,q
let x be bound_QC-variable; :: thesis: ( p <==> q implies All x,p <==> All x,q )
assume p <==> q ; :: thesis: All x,p <==> All x,q
then ( p => q is valid & q => p is valid ) by Th50;
then ( All x,(p => q) is valid & All x,(q => p) is valid ) by CQC_THE2:26;
then ( (All x,p) => (All x,q) is valid & (All x,q) => (All x,p) is valid ) by CQC_THE2:35;
hence All x,p <==> All x,q by Th50; :: thesis: verum