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

Theorem mtoi 653
 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 652 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 603  ax-in2 604 This theorem is referenced by:  mtbii  663  mtbiri  664  pwnss  4083  nsuceq0g  4340  abnex  4368  reg2exmidlema  4449  ordsuc  4478  onnmin  4483  ssnel  4484  ordtri2or2exmid  4486  reg3exmidlemwe  4493  acexmidlemab  5768  reldmtpos  6150  dmtpos  6153  2pwuninelg  6180  onunsnss  6805  snon0  6824  exmidomni  7014  pr2ne  7055  ltexprlemdisj  7428  recexprlemdisj  7452  caucvgprlemnkj  7488  caucvgprprlemnkltj  7511  caucvgprprlemnkeqj  7512  caucvgprprlemnjltk  7513  inelr  8360  rimul  8361  recgt0  8622  zfz1iso  10598  isprm2  11811  nprmdvds1  11833  divgcdodd  11834  coprm  11835  coseq0q4123  12939  pwle2  13300  exmid1stab  13302  nninfalllem1  13312  nninfall  13313  nninfsellemqall  13320
 Copyright terms: Public domain W3C validator