ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtoi Unicode 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  |-  -.  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 599 1  |-  ( ph  ->  -.  ps )
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  3940  nsuceq0g  4183  reg2exmidlema  4287  ordsuc  4315  onnmin  4320  ssnel  4321  onpsssuc  4323  ordtri2or2exmid  4324  reg3exmidlemwe  4331  acexmidlemab  5534  reldmtpos  5899  dmtpos  5902  2pwuninelg  5929  onunsnss  6386  snon0  6387  ltexprlemdisj  6762  recexprlemdisj  6786  caucvgprlemnkj  6822  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  inelr  7649  rimul  7650  recgt0  7891
  Copyright terms: Public domain W3C validator