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

Theorem mtod 589
 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 586 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 544  ax-in2 545 This theorem is referenced by:  mtoi  590  mtand  591  mtbid  597  mtbird  598  po2nr  4046  po3nr  4047  sotricim  4060  elirr  4266  ordn2lp  4269  en2lp  4278  nndomo  6326  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  caucvgprprlemaddq  6806  msqge0  7607  mulge0  7610  squeeze0  7870  elnn0z  8258  fznlem  8905  frec2uzf1od  9192  bj-nnen2lp  10079
 Copyright terms: Public domain W3C validator