Goal forall A B C, (A -> B -> C)-> (A -> B) -> (A->C).
intros A B C H1 H2 H3.
apply H1.
exact H3.
apply H2.
exact H3.
Qed.

(** About classical logic *)

Lemma neg3 : forall A, ~ ~ ~ A -> ~ A.

Definition class (A : Prop) : Prop := ~ ~ A -> A.

Definition orc (A B:Prop) := ~ (~ A /\ ~ B).

Lemma orc_left : forall (A B:Prop), A -> orc A B.

Lemma orc_right : forall (A B:Prop), B -> orc A B.

Lemma orc_elim : forall (A B C:Prop), 
   (A -> C) -> (B -> C) -> orc A B -> class C -> C.