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  4351  phpm  6865  diffisn  6893  tridc  6899  nnnninfeq  7126  pm54.43  7189  addcanprleml  7613  addcanprlemu  7614  iseqf1olemklt  10485  isprm5lem  12141  pw2dvdseulemle  12167  sqne2sq  12177  pythagtriplem4  12268  pythagtriplem11  12274  pythagtriplem13  12276  ctinfomlemom  12428  ivthinc  14124  pwle2  14751
  Copyright terms: Public domain W3C validator