ILE Home 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  2760  sspssn  3045  neldifsn  3494  nvel  3886  nlim0  4118  snnex  4168  onprc  4261  dtruex  4268  ordsoexmid  4271  nprrel  4364  0xp  4398  iprc  4578  son2lpi  4699  nfunv  4911  0fv  5186  acexmidlema  5481  acexmidlemb  5482  acexmidlemab  5484  mpt20  5552  php5dom  6303  0nnq  6434  0npr  6553  1ne0sr  6823  pnfnre  7038  mnfnre  7039  ine0  7361  inelr  7542  1nuz2  8506  0nrp  8578  bj-nvel  9881
  Copyright terms: Public domain W3C validator