A binary logical connective, denoted

\begin{equation*} P \implies Q \qor Q \impliedby P \end{equation*}

where	\(P\)	is the antecedent
	\(Q\)	is the consequent,

and read

	“if \(P\), then \(Q\)”
or	“\(Q\) if \(P\)”
or	“\(P\) implies \(Q\)”,

that is true if and only if

\(P\) and \(Q\) are true or \(P\) is false,

so equivalent to

\begin{equation*} \lnot P \lor Q. \end{equation*}

Equivalent to its contrapositive but not to its converse.

[1, Sec. 0.2], [2, Sec. 5.1]

---