(* Wersja rozszerzona 8 marca *) Variables p q r s t : Prop. Goal (p/\q -> r) <-> (p -> q -> r). split. intros. apply H. split. assumption. assumption. intros. destruct H0. apply H. assumption. assumption. Qed. Goal ~(p\/q) -> ~p/\~q. intro. split. intro. apply H. left. apply H0. intro;apply H;right;apply H0. Qed. Goal p\/q -> ~p -> q. intros. elim H. intro. exfalso. apply H0. apply H1. intro;assumption. Qed. Goal p -> p. Goal p -> (p -> q) -> q. Goal p -> ~~p. Goal (p->q) -> (q->r) -> p -> r. Goal (p->q) -> (~q -> ~p). Goal (p\/q -> r) -> (p -> r) /\ (q -> r). Goal (p -> q -> r) -> (p -> q) -> p -> r. Goal False -> p. Goal p \/~p. Goal ~~(p\/~p). Goal (((p -> q)-> p) -> p). Goal (((((p -> q)-> p) -> p) -> q) -> q). Goal (p -> q) -> (~p -> q) -> q. Goal (p -> ~q) -> (~p -> ~q) -> ~q.