theorem :: QC_LANG2:22

for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t being bound_QC-variable of A st All (x,y,z,p) = All (t,q) holds
( x = t & All (y,z,p) = q ) by Th5;