Section LogicMythCoherentGround.

Variables P Q R : Prop.

Theorem consequence
    (hP : P)
    (hPQ : P <-> Q)
    (hQNR : Q <-> ~ R) :
    (P /\ Q) /\ ~ R.
Proof.
  split.
  - split.
    + exact hP.
    + exact (proj1 hPQ hP).
  - exact (proj1 hQNR (proj1 hPQ hP)).
Qed.

Print Assumptions consequence.

End LogicMythCoherentGround.