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  4352  phpm  6868  diffisn  6896  tridc  6902  nnnninfeq  7129  pm54.43  7192  addcanprleml  7616  addcanprlemu  7617  iseqf1olemklt  10488  isprm5lem  12144  pw2dvdseulemle  12170  sqne2sq  12180  pythagtriplem4  12271  pythagtriplem11  12277  pythagtriplem13  12279  ctinfomlemom  12431  lssvancl1  13465  ivthinc  14282  pwle2  14910
  Copyright terms: Public domain W3C validator