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

Theorem mto 636
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 613 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 588  ax-in2 589
This theorem is referenced by:  mtbi  644  pm3.2ni  787  pm5.16  798  intnan  899  intnanr  900  equidqe  1497  nexr  1655  ru  2881  neldifsn  3623  nvel  4031  nlim0  4286  snnex  4339  onprc  4437  dtruex  4444  ordsoexmid  4447  nprrel  4554  0xp  4589  iprc  4777  son2lpi  4905  nfunv  5126  0fv  5424  acexmidlema  5733  acexmidlemb  5734  acexmidlemab  5736  mpo0  5809  php5dom  6725  fi0  6831  0nnq  7140  0npr  7259  1ne0sr  7542  pnfnre  7775  mnfnre  7776  ine0  8124  inelr  8314  nn0nepnf  9016  1nuz2  9368  0nrp  9445  inftonninf  10182  eirr  11412  odd2np1  11497  n2dvds1  11536  1nprm  11722  structcnvcnv  11902  fvsetsid  11920  0ntop  12101  topnex  12182  bj-nnst  12891  bj-nvel  13022  pwle2  13120  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator