\begin{definition}[Definition:Semantic Consequence/Boolean Interpretations]
<section notitle="true" name="tc">
Let $\FF$ be a collection of WFFs of propositional logic.
Then a WFF $\mathbf A$ is a '''semantic consequence''' of $\FF$ {{iff}}:
:$v \models_{\mathrm{BI}} \FF$ implies $v \models_{\mathrm{BI}} \mathbf A$
where $\models_{\mathrm{BI}}$ is the models relation.
</section>
{{transclude:Definition:Semantic Consequence/Boolean Interpretations/Single Formula
  |section = tc
  |title = Semantic Consequence of Single Formula
  |header = 3
  |link = true
  |increase = 1
}}
\end{definition}