Mathematical conjectures and theorems are most often of the form P(x) ? Q(x), meaning ?x,P(x) ? Q(x). The hidden quantifier ?x is crucial in understanding the implication as a statement with a truth value. Here P(x) and Q(x) alone are only predicates, without truth values, since they contain unquantified variables. But standard textbook instruction on implication, in particular in writing negations, relies mainly on truth tables, treating P and Q as statements themselves with their own truth values. The lack of careful and thorough explanations on handling implications of the form P(x) ? Q(x) creates difficulties for students, in particular in proof by contradiction, where one begins with the negation of the statement to be proved. Through analysis of interesting errors involving hidden quantifiers in implication, this article offers ways to improve standard instruction to treat these quantifiers correctly and explicitly.