Goal forall A B C, (A -> B -> C)-> (A -> B) -> (A->C).
(* auto. *)
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.
(* tauto. *)
intros A H x.
apply H.
intro H1.
apply H1; trivial.
Save.

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.
(* unfold orc; tauto. *)
intros A B H1 H2.
destruct H2 as (Hna,Hnb).
apply Hna; trivial.
Save.

Lemma orc_right : forall (A B:Prop), B -> orc A B.
(* unfold orc; tauto. *)
intros A B H1 H2.
destruct H2 as (Hna,Hnb).
apply Hnb; trivial.
Save.

Lemma orc_elim : forall (A B C:Prop), 
   (A -> C) -> (B -> C) -> orc A B -> class C -> C.
(* unfold orc,class; tauto. *)
intros A B C HA HB Hor Hc.
apply Hc.
intro Hnc.
apply Hor.
split.
intro H; apply Hnc; auto.
intro H; apply Hnc; auto.
Save.