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  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  msqge0  7400  mulge0  7403  squeeze0  7651  elnn0z  8034  fznlem  8675  frec2uzf1od  8873  bj-nnen2lp  9408
  Copyright terms: Public domain W3C validator