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

Theorem mtod 588
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1 (φ → ¬ χ)
mtod.2 (φ → (ψχ))
Assertion
Ref Expression
mtod (φ → ¬ ψ)

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2 (φ → (ψχ))
2 mtod.1 . . 3 (φ → ¬ χ)
32a1d 22 . 2 (φ → (ψ → ¬ χ))
41, 3pm2.65d 585 1 (φ → ¬ ψ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 544  ax-in2 545
This theorem is referenced by:  mtoi  589  mtand  590  mtbid  596  mtbird  597  po2nr  4037  po3nr  4038  sotricim  4051  elirr  4224  en2lp  4232  msqge0  7360  mulge0  7363  squeeze0  7611  elnn0z  7994  fznlem  8635  frec2uzf1od  8833  bj-nnen2lp  9342
  Copyright terms: Public domain W3C validator