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.

(Levin 2021, sec. 0.2; Poole and Mackworth 2017, sec. 5.1)

---

• Synonyms
• Truth table