The following lemma is sometimes very helpful in proving implications in mathematics. It uses the fact that the implication $x\Rightarrow y$ can be represented by the disjunction $\neg x\vee y$.
Any implication $x\Rightarrow y$ is equivalent to the disjunction of the negated antecedent $\neg x$ and the consequent $y$, formally $$(x\Rightarrow y)\Longleftrightarrow (\neg x \vee y).$$
This lemma is a little bit surprising because, in natural language, it is not intuitive. Consider for instance the following propositions:
$x=$"Socrates is human."
$y=$"Socrates is mortal."
Then the following compound propositions are equivalent:
$x\Rightarrow y$: "If Socrates is human, then Socrates is mortal."
$\neg x \vee y$: "Socrates is not human, or Socrates is mortal."
Proofs: 1