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

Theorem mtoi 623
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1 ¬ 𝜒
mtoi.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtoi (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3 ¬ 𝜒
21a1i 9 . 2 (𝜑 → ¬ 𝜒)
3 mtoi.2 . 2 (𝜑 → (𝜓𝜒))
42, 3mtod 622 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 577  ax-in2 578
This theorem is referenced by:  mtbii  632  mtbiri  633  pwnss  3959  nsuceq0g  4209  reg2exmidlema  4313  ordsuc  4342  onnmin  4347  ssnel  4348  ordtri2or2exmid  4350  reg3exmidlemwe  4357  acexmidlemab  5585  reldmtpos  5950  dmtpos  5953  2pwuninelg  5980  onunsnss  6554  snon0  6570  exmidomni  6703  pr2ne  6723  ltexprlemdisj  7068  recexprlemdisj  7092  caucvgprlemnkj  7128  caucvgprprlemnkltj  7151  caucvgprprlemnkeqj  7152  caucvgprprlemnjltk  7153  inelr  7961  rimul  7962  recgt0  8205  isprm2  10879  nprmdvds1  10901  divgcdodd  10902  coprm  10903
  Copyright terms: Public domain W3C validator