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

Theorem mto 588
 Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mto.1 ¬ 𝜓
mto.2 (𝜑𝜓)
Assertion
Ref Expression
mto ¬ 𝜑

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2 (𝜑𝜓)
2 mto.1 . . 3 ¬ 𝜓
32a1i 9 . 2 (𝜑 → ¬ 𝜓)
41, 3pm2.65i 568 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:  mtbi  595  pm3.2ni  726  pm5.16  737  intnan  838  intnanr  839  equidqe  1425  nexr  1582  ru  2763  sspssn  3048  neldifsn  3497  nvel  3889  nlim0  4131  snnex  4181  onprc  4276  dtruex  4283  ordsoexmid  4286  nprrel  4386  0xp  4420  iprc  4600  son2lpi  4721  nfunv  4933  0fv  5208  acexmidlema  5503  acexmidlemb  5504  acexmidlemab  5506  mpt20  5574  php5dom  6325  0nnq  6462  0npr  6581  1ne0sr  6851  pnfnre  7067  mnfnre  7068  ine0  7391  inelr  7575  1nuz2  8543  0nrp  8616  bj-nvel  10017
 Copyright terms: Public domain W3C validator