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.