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

Theorem mtod 622
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 619 1 (𝜑 → ¬ 𝜓)
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 577  ax-in2 578
This theorem is referenced by:  mtoi  623  mtand  624  mtbid  630  mtbird  631  po2nr  4100  po3nr  4101  sotricim  4114  elirr  4320  ordn2lp  4324  en2lp  4333  tfr1onlemsucaccv  6038  tfrcllemsucaccv  6051  nndomo  6510  fnfi  6571  cauappcvgprlemladdru  7118  cauappcvgprlemladdrl  7119  caucvgprlemladdrl  7140  caucvgprprlemaddq  7170  msqge0  7993  mulge0  7996  squeeze0  8259  elnn0z  8659  fznlem  9350  frec2uzf1od  9702  facndiv  9982  isumrblem  10573  alzdvds  10635  fzm1ndvds  10637  fzo0dvdseq  10638  rpdvds  10861  nonsq  10965  bj-nnen2lp  11192
  Copyright terms: Public domain W3C validator