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

Theorem mto 587
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 567 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  594  pm3.2ni  725  pm5.16  736  intnan  837  intnanr  838  equidqe  1422  nexr  1579  ru  2757  sspssn  3042  neldifsn  3488  nvel  3880  nlim0  4097  snnex  4147  onprc  4230  dtruex  4237  ordsoexmid  4240  nprrel  4329  0xp  4363  iprc  4543  son2lpi  4664  nfunv  4876  0fv  5151  acexmidlema  5446  acexmidlemb  5447  acexmidlemab  5449  mpt20  5516  0nnq  6348  0npr  6466  1ne0sr  6694  pnfnre  6864  mnfnre  6865  ine0  7187  inelr  7368  1nuz2  8319  0nrp  8391  bj-nvel  9352
  Copyright terms: Public domain W3C validator