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 A1: p <==> q ; :: thesis: All x,p <==> All x,q
then q => p is valid by Th50;
then All x,(q => p) is valid by CQC_THE2:26;
then A2: (All x,q) => (All x,p) is valid by CQC_THE2:35;
p => q is valid by A1, Th50;
then All x,(p => q) is valid by CQC_THE2:26;
then (All x,p) => (All x,q) is valid by CQC_THE2:35;
hence All x,p <==> All x,q by A2, Th50; :: thesis: verum