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

Theorem mtod 664
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 661 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 615  ax-in2 616
This theorem is referenced by:  mtoi  665  mtand  666  mtbid  673  mtbird  674  pwntru  4211  po2nr  4321  po3nr  4322  sotricim  4335  elirr  4552  ordn2lp  4556  en2lp  4565  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  nndomo  6878  fnfi  6950  difinfsnlem  7112  nninfwlpoimlemginf  7188  2omotaplemap  7270  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  caucvgprlemladdrl  7691  caucvgprprlemaddq  7721  msqge0  8587  mulge0  8590  squeeze0  8875  elnn0z  9280  fznlem  10055  frec2uzf1od  10420  facndiv  10733  sumrbdclem  11399  prodrbdclem  11593  alzdvds  11874  fzm1ndvds  11876  fzo0dvdseq  11877  rpdvds  12113  nonsq  12221  prmdiv  12249  odzdvds  12259  pcprendvds  12304  pcprendvds2  12305  pcpremul  12307  pcdvdsb  12333  pockthlem  12368  1arith  12379  ennnfonelemim  12439  bldisj  14254  lgsdilem2  14790  lgsne0  14792  lgseisenlem1  14803  lgseisenlem2  14804  bj-nnen2lp  15059  pwtrufal  15101  refeq  15130
  Copyright terms: Public domain W3C validator