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

Theorem mtoi 638
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1  |-  -.  ch
mtoi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mtoi  |-  ( ph  ->  -.  ps )

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3  |-  -.  ch
21a1i 9 . 2  |-  ( ph  ->  -.  ch )
3 mtoi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mtod 637 1  |-  ( ph  ->  -.  ps )
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 588  ax-in2 589
This theorem is referenced by:  mtbii  648  mtbiri  649  pwnss  4053  nsuceq0g  4310  abnex  4338  reg2exmidlema  4419  ordsuc  4448  onnmin  4453  ssnel  4454  ordtri2or2exmid  4456  reg3exmidlemwe  4463  acexmidlemab  5736  reldmtpos  6118  dmtpos  6121  2pwuninelg  6148  onunsnss  6773  snon0  6792  exmidomni  6982  pr2ne  7016  ltexprlemdisj  7382  recexprlemdisj  7406  caucvgprlemnkj  7442  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemnjltk  7467  inelr  8314  rimul  8315  recgt0  8576  zfz1iso  10552  isprm2  11725  nprmdvds1  11747  divgcdodd  11748  coprm  11749  coseq0q4123  12842  pwle2  13120  exmid1stab  13122  nninfalllem1  13130  nninfall  13131  nninfsellemqall  13138
  Copyright terms: Public domain W3C validator