ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtand GIF version

Theorem mtand 665
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypotheses
Ref Expression
mtand.1 (𝜑 → ¬ 𝜒)
mtand.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mtand (𝜑 → ¬ 𝜓)

Proof of Theorem mtand
StepHypRef Expression
1 mtand.1 . 2 (𝜑 → ¬ 𝜒)
2 mtand.2 . . 3 ((𝜑𝜓) → 𝜒)
32ex 115 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 663 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 614  ax-in2 615
This theorem is referenced by:  frirrg  4350  phpm  6864  diffisn  6892  tridc  6898  nnnninfeq  7125  pm54.43  7188  addcanprleml  7612  addcanprlemu  7613  iseqf1olemklt  10484  isprm5lem  12140  pw2dvdseulemle  12166  sqne2sq  12176  pythagtriplem4  12267  pythagtriplem11  12273  pythagtriplem13  12275  ctinfomlemom  12427  ivthinc  14091  pwle2  14718
  Copyright terms: Public domain W3C validator