import Lean

namespace HunterAuthored.LogicMythCoherentGround

theorem consequence
    (P Q R : Prop)
    (hP : P)
    (hPQ : P ↔ Q)
    (hQNR : Q ↔ ¬ R) :
    (P ∧ Q) ∧ ¬ R := by
  have hQ : Q := hPQ.mp hP
  have hNotR : ¬ R := hQNR.mp hQ
  exact ⟨⟨hP, hQ⟩, hNotR⟩

#print axioms consequence

end HunterAuthored.LogicMythCoherentGround