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

Theorem mtod 637
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 634 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 588  ax-in2 589
This theorem is referenced by:  mtoi  638  mtand  639  mtbid  646  mtbird  647  pwntru  4092  po2nr  4201  po3nr  4202  sotricim  4215  elirr  4426  ordn2lp  4430  en2lp  4439  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  nndomo  6726  fnfi  6793  difinfsnlem  6952  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  caucvgprprlemaddq  7484  msqge0  8346  mulge0  8349  squeeze0  8630  elnn0z  9035  fznlem  9789  frec2uzf1od  10147  facndiv  10453  sumrbdclem  11113  alzdvds  11479  fzm1ndvds  11481  fzo0dvdseq  11482  rpdvds  11707  nonsq  11812  ennnfonelemim  11864  bldisj  12497  bj-nnen2lp  13079  pwtrufal  13119  refeq  13150
  Copyright terms: Public domain W3C validator