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  2828  neldifsn  3555  nvel  3949  nlim0  4197  snnex  4247  onprc  4343  dtruex  4350  ordsoexmid  4353  nprrel  4454  0xp  4488  iprc  4671  son2lpi  4797  nfunv  5014  0fv  5304  acexmidlema  5606  acexmidlemb  5607  acexmidlemab  5609  mpt20  5677  php5dom  6533  0nnq  6870  0npr  6989  1ne0sr  7259  pnfnre  7476  mnfnre  7477  ine0  7819  inelr  8005  nn0nepnf  8680  1nuz2  9028  0nrp  9102  inftonninf  9778  odd2np1  10779  n2dvds1  10818  1nprm  11002  bj-nvel  11257  exmidsbthrlem  11381
  Copyright terms: Public domain W3C validator