theory Logic_Myth_Coherent_Ground
  imports Main
begin

theorem consequence:
  assumes hP: P
    and hPQ: "P ⟷ Q"
    and hQNR: "Q ⟷ ¬ R"
  shows "(P ∧ Q) ∧ ¬ R"
proof -
  have hQ: Q
    using hP hPQ by blast
  have hNotR: "¬ R"
    using hQ hQNR by blast
  show ?thesis
    using hP hQ hNotR by blast
qed

end