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

Theorem mtoi 600
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 599 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 554  ax-in2 555
This theorem is referenced by:  mtbii  609  mtbiri  610  pwnss  3939  nsuceq0g  4182  reg2exmidlema  4286  ordsuc  4314  onnmin  4319  ssnel  4320  onpsssuc  4322  ordtri2or2exmid  4323  reg3exmidlemwe  4330  acexmidlemab  5533  reldmtpos  5898  dmtpos  5901  2pwuninelg  5928  onunsnss  6385  snon0  6386  ltexprlemdisj  6761  recexprlemdisj  6785  caucvgprlemnkj  6821  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemnjltk  6846  inelr  7648  rimul  7649  recgt0  7890
  Copyright terms: Public domain W3C validator