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

Theorem mtod 599
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 596 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:  mtoi  600  mtand  601  mtbid  607  mtbird  608  po2nr  4074  po3nr  4075  sotricim  4088  elirr  4294  ordn2lp  4297  en2lp  4306  nndomo  6357  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemladdrl  6834  caucvgprprlemaddq  6864  msqge0  7681  mulge0  7684  squeeze0  7945  elnn0z  8315  fznlem  9007  frec2uzf1od  9356  facndiv  9607  alzdvds  10166  fzm1ndvds  10168  fzo0dvdseq  10169  bj-nnen2lp  10466
  Copyright terms: Public domain W3C validator