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

Theorem mtoi 625
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 624 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 579  ax-in2 580
This theorem is referenced by:  mtbii  634  mtbiri  635  pwnss  3994  nsuceq0g  4245  reg2exmidlema  4350  ordsuc  4379  onnmin  4384  ssnel  4385  ordtri2or2exmid  4387  reg3exmidlemwe  4394  acexmidlemab  5646  reldmtpos  6018  dmtpos  6021  2pwuninelg  6048  onunsnss  6627  snon0  6645  exmidomni  6798  pr2ne  6820  ltexprlemdisj  7165  recexprlemdisj  7189  caucvgprlemnkj  7225  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemnjltk  7250  inelr  8061  rimul  8062  recgt0  8311  zfz1iso  10246  isprm2  11377  nprmdvds1  11399  divgcdodd  11400  coprm  11401  nninfalllem1  11899  nninfall  11900  nninfsellemqall  11907
  Copyright terms: Public domain W3C validator