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

Theorem mtoi 654
 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 653 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 604  ax-in2 605 This theorem is referenced by:  mtbii  664  mtbiri  665  pwnss  4093  nsuceq0g  4351  abnex  4379  reg2exmidlema  4460  ordsuc  4489  onnmin  4494  ssnel  4495  ordtri2or2exmid  4497  reg3exmidlemwe  4504  acexmidlemab  5780  reldmtpos  6162  dmtpos  6165  2pwuninelg  6192  onunsnss  6822  snon0  6841  exmidomni  7035  pr2ne  7077  ltexprlemdisj  7467  recexprlemdisj  7491  caucvgprlemnkj  7527  caucvgprprlemnkltj  7550  caucvgprprlemnkeqj  7551  caucvgprprlemnjltk  7552  inelr  8399  rimul  8400  recgt0  8661  zfz1iso  10645  isprm2  11870  nprmdvds1  11892  divgcdodd  11893  coprm  11894  coseq0q4123  12999  pwle2  13410  exmid1stab  13412  nninfalllem1  13422  nninfall  13423  nninfsellemqall  13430
 Copyright terms: Public domain W3C validator