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

Theorem mtoi 589
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 588 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  598  mtbiri  599  pwnss  3903  nsuceq0g  4121  ordsuc  4241  onnmin  4244  ssnel  4245  onpsssuc  4247  acexmidlemab  5449  reldmtpos  5809  dmtpos  5812  2pwuninelg  5839  ltexprlemdisj  6579  recexprlemdisj  6601  inelr  7348  rimul  7349  recgt0  7577
  Copyright terms: Public domain W3C validator