ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mto Unicode 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  |-  -.  ps
mto.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
mto  |-  -.  ph

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2  |-  ( ph  ->  ps )
2 mto.1 . . 3  |-  -.  ps
32a1i 9 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 578 1  |-  -.  ph
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  2786  sspssn  3076  neldifsn  3525  nvel  3917  nlim0  4159  snnex  4209  onprc  4304  dtruex  4311  ordsoexmid  4314  nprrel  4414  0xp  4448  iprc  4628  son2lpi  4749  nfunv  4961  0fv  5236  acexmidlema  5531  acexmidlemb  5532  acexmidlemab  5534  mpt20  5602  php5dom  6356  0nnq  6520  0npr  6639  1ne0sr  6909  pnfnre  7126  mnfnre  7127  ine0  7463  inelr  7649  1nuz2  8640  0nrp  8714  odd2np1  10184  n2dvds1  10224  bj-nvel  10404
  Copyright terms: Public domain W3C validator