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

Theorem mtod 625
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1  |-  ( ph  ->  -.  ch )
mtod.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mtod  |-  ( ph  ->  -.  ps )

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 mtod.1 . . 3  |-  ( ph  ->  -.  ch )
32a1d 22 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
41, 3pm2.65d 622 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 580  ax-in2 581
This theorem is referenced by:  mtoi  626  mtand  627  mtbid  633  mtbird  634  po2nr  4145  po3nr  4146  sotricim  4159  elirr  4370  ordn2lp  4374  en2lp  4383  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  nndomo  6634  fnfi  6700  cauappcvgprlemladdru  7269  cauappcvgprlemladdrl  7270  caucvgprlemladdrl  7291  caucvgprprlemaddq  7321  msqge0  8147  mulge0  8150  squeeze0  8419  elnn0z  8817  fznlem  9509  frec2uzf1od  9867  facndiv  10201  isumrblem  10819  alzdvds  11187  fzm1ndvds  11189  fzo0dvdseq  11190  rpdvds  11413  nonsq  11517  bj-nnen2lp  12115
  Copyright terms: Public domain W3C validator