Section Exercise_5_3. Variables P Q R : Prop. Theorem ex1 : ~False. Proof. intro. assumption. Qed. Theorem ex2 : ~~~P -> ~P. Proof. intros. intro. elim H. intro. elim H1. assumption. Qed. Theorem ex3 : ~~~P -> P -> Q. Proof. intros. elim H. intro. elim H1. assumption. Qed. Theorem ex4 : (P->Q)->~Q->~P. Proof. intros. intro. elim H0. apply H. assumption. Qed. Theorem ex5 : (P->Q)->(P->~Q)->P->R. Proof. intros. assert (H2 : P); [ assumption | ]. apply H0 in H1. apply H in H2. contradiction. Qed. End Exercise_5_3.