Theorem impl_th1 : ∀ P Q R : Prop,
    (P → Q) → (Q → R) → (P → R).
Proof.
Admitted.

Theorem impl_th2 : ∀ P Q R : Prop,
    (P → Q → R) → (Q → P → R).
Proof.
Admitted.

Theorem impl_th3 : ∀ P Q R : Prop,
    (P → Q → R) → (P → Q) → (P → R).
Proof.
Admitted.

Theorem contrapositive : ∀ P Q : Prop,
    (P → Q) → (~Q → ¬P).
Proof.
Admitted.

Theorem not_both_true_and_false : ∀ P : Prop,
    ~(P ∧ ¬P).
Proof.
Admitted.

Theorem neg_neg_neg_impl_neg : ∀ P : Prop,
    ~~~P → ¬P.
Proof.
Admitted.

Theorem de_morgan_not_or : ∀ (P Q : Prop),
    ¬ (P ∨ Q) → ¬P ∧ ¬Q.
Proof.
Admitted.

Theorem or_distributes_over_and : ∀ P Q R : Prop,
  P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R).
Proof.
Admitted.

Theorem dist_exists_or : ∀ (X:Type) (P Q : X → Prop),
  (∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ (∃ x, Q x).
Proof.
Admitted.