Skip to content

Instantly share code, notes, and snippets.

@KeenS
Created April 7, 2014 13:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save KeenS/10019999 to your computer and use it in GitHub Desktop.
Save KeenS/10019999 to your computer and use it in GitHub Desktop.
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
intros.
destruct H.
intro.
apply H.
apply H0.
apply H1.
Qed.
Copy link

ghost commented Apr 7, 2014

highlights

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment