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

Theorem mto 621
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 601 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 577  ax-in2 578
This theorem is referenced by:  mtbi  628  pm3.2ni  760  pm5.16  771  intnan  874  intnanr  875  equidqe  1468  nexr  1625  ru  2827  neldifsn  3547  nvel  3940  nlim0  4188  snnex  4238  onprc  4334  dtruex  4341  ordsoexmid  4344  nprrel  4445  0xp  4479  iprc  4662  son2lpi  4786  nfunv  5003  0fv  5287  acexmidlema  5585  acexmidlemb  5586  acexmidlemab  5588  mpt20  5656  php5dom  6512  0nnq  6844  0npr  6963  1ne0sr  7233  pnfnre  7450  mnfnre  7451  ine0  7793  inelr  7979  nn0nepnf  8654  1nuz2  9002  0nrp  9076  inftonninf  9750  odd2np1  10667  n2dvds1  10706  1nprm  10890  bj-nvel  11145  exmidsbthrlem  11268
  Copyright terms: Public domain W3C validator