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

Theorem mtoi 590
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 589 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:  mtbii  599  mtbiri  600  pwnss  3909  nsuceq0g  4142  ordsuc  4272  onnmin  4277  ssnel  4278  onpsssuc  4280  ordtri2or2exmid  4281  acexmidlemab  5484  reldmtpos  5846  dmtpos  5849  2pwuninelg  5876  ltexprlemdisj  6676  recexprlemdisj  6700  caucvgprlemnkj  6736  caucvgprprlemnkltj  6759  caucvgprprlemnkeqj  6760  caucvgprprlemnjltk  6761  inelr  7542  rimul  7543  recgt0  7783
  Copyright terms: Public domain W3C validator