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

Theorem mto 598
 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 578 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 554  ax-in2 555 This theorem is referenced by:  mtbi  605  pm3.2ni  737  pm5.16  748  intnan  849  intnanr  850  equidqe  1441  nexr  1598  ru  2785  sspssn  3075  neldifsn  3524  nvel  3916  nlim0  4158  snnex  4208  onprc  4303  dtruex  4310  ordsoexmid  4313  nprrel  4413  0xp  4447  iprc  4627  son2lpi  4748  nfunv  4960  0fv  5235  acexmidlema  5530  acexmidlemb  5531  acexmidlemab  5533  mpt20  5601  php5dom  6355  0nnq  6519  0npr  6638  1ne0sr  6908  pnfnre  7125  mnfnre  7126  ine0  7462  inelr  7648  1nuz2  8639  0nrp  8713  odd2np1  10183  n2dvds1  10223  bj-nvel  10383
 Copyright terms: Public domain W3C validator