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

Theorem mtod 635
 Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1 (𝜑 → ¬ 𝜒)
mtod.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtod (𝜑 → ¬ 𝜓)

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2 (𝜑 → (𝜓𝜒))
2 mtod.1 . . 3 (𝜑 → ¬ 𝜒)
32a1d 22 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
41, 3pm2.65d 632 1 (𝜑 → ¬ 𝜓)
 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 586  ax-in2 587 This theorem is referenced by:  mtoi  636  mtand  637  mtbid  644  mtbird  645  pwntru  4090  po2nr  4199  po3nr  4200  sotricim  4213  elirr  4424  ordn2lp  4428  en2lp  4437  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  nndomo  6724  fnfi  6791  difinfsnlem  6950  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  caucvgprprlemaddq  7480  msqge0  8341  mulge0  8344  squeeze0  8622  elnn0z  9021  fznlem  9772  frec2uzf1od  10130  facndiv  10436  sumrbdclem  11096  alzdvds  11459  fzm1ndvds  11461  fzo0dvdseq  11462  rpdvds  11687  nonsq  11791  ennnfonelemim  11843  bldisj  12476  bj-nnen2lp  12986  pwtrufal  13026  refeq  13057
 Copyright terms: Public domain W3C validator