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

Theorem mto 623
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 603 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 579  ax-in2 580
This theorem is referenced by:  mtbi  630  pm3.2ni  762  pm5.16  773  intnan  876  intnanr  877  equidqe  1470  nexr  1627  ru  2837  neldifsn  3565  nvel  3964  nlim0  4212  snnex  4262  onprc  4358  dtruex  4365  ordsoexmid  4368  nprrel  4472  0xp  4506  iprc  4689  son2lpi  4815  nfunv  5033  0fv  5323  acexmidlema  5625  acexmidlemb  5626  acexmidlemab  5628  mpt20  5700  php5dom  6559  0nnq  6902  0npr  7021  1ne0sr  7291  pnfnre  7508  mnfnre  7509  ine0  7851  inelr  8037  nn0nepnf  8714  1nuz2  9062  0nrp  9136  inftonninf  9812  odd2np1  10966  n2dvds1  11005  1nprm  11189  bj-nvel  11445  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator