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

Theorem mtod 652
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 649 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 603  ax-in2 604
This theorem is referenced by:  mtoi  653  mtand  654  mtbid  661  mtbird  662  pwntru  4117  po2nr  4226  po3nr  4227  sotricim  4240  elirr  4451  ordn2lp  4455  en2lp  4464  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  nndomo  6751  fnfi  6818  difinfsnlem  6977  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  caucvgprprlemaddq  7509  msqge0  8371  mulge0  8374  squeeze0  8655  elnn0z  9060  fznlem  9814  frec2uzf1od  10172  facndiv  10478  sumrbdclem  11138  prodrbdclem  11333  alzdvds  11541  fzm1ndvds  11543  fzo0dvdseq  11544  rpdvds  11769  nonsq  11874  ennnfonelemim  11926  bldisj  12559  bj-nnen2lp  13141  pwtrufal  13181  refeq  13212
  Copyright terms: Public domain W3C validator