The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps.  The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and checking for alpha-equivalence (or maybe alpha,eta-equivalence).