Section Minimal_propositional_logic.
Variables P Q R T: Prop.
Theorem imp_trans: 
(P -> Q) -> (Q -> R) -> (P -> R).
intro.
intro.
intro p.
apply H0.
apply H.
assumption.
Qed.
Print imp_trans.


Theorem imp_trans2: 
(P -> Q) -> (Q -> R) -> (P -> R).
auto.
Qed.
Print imp_trans2.

Check conj.

Theorem and_commutative: 
P /\ Q -> Q /\ P.
intro H.
elim H.
split.
assumption.
assumption.
Qed.
Print and_commutative.

Theorem or_distr:
P \/ (Q /\ R)  ->  (P\/Q)/\(P \/ R).
Proof.
tauto.
Qed.
Print or_distr.