Variables A B C D: Prop.

Theorem ex2_1: A/\B->B/\A.
intro.
split.
destruct H.
apply H0.
destruct H.
apply H.
Qed.

Theorem ex2_4: (A/\B->C) -> (A->B->C).
intros.
apply H.
split.
apply H0.
apply H1.
Qed.

Theorem ex2_4bis: (A->B/\C)->A->B.
intro.
intro.
destruct H.
apply H0.
apply H.
Qed.

Theorem ex2_5: (A->B->C)->(A/\B->C).
intros.
apply H.
destruct H0.
apply H0.
destruct H0.
apply H1.
Qed.

Theorem ex2_6: (A->B) /\ (C->D) /\ A /\ C -> B /\ D.
intros.
split.
destruct H.
apply H.
destruct H0.
destruct H1.
apply H1.
destruct H.
destruct H0.
apply H0.
destruct H1.
apply H2.
Qed.