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

Theorem mto 634
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 611 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 586  ax-in2 587
This theorem is referenced by:  mtbi  642  pm3.2ni  785  pm5.16  796  intnan  897  intnanr  898  equidqe  1495  nexr  1653  ru  2879  neldifsn  3621  nvel  4029  nlim0  4284  snnex  4337  onprc  4435  dtruex  4442  ordsoexmid  4445  nprrel  4552  0xp  4587  iprc  4775  son2lpi  4903  nfunv  5124  0fv  5422  acexmidlema  5731  acexmidlemb  5732  acexmidlemab  5734  mpo0  5807  php5dom  6723  fi0  6829  0nnq  7136  0npr  7255  1ne0sr  7538  pnfnre  7771  mnfnre  7772  ine0  8120  inelr  8309  nn0nepnf  9002  1nuz2  9352  0nrp  9428  inftonninf  10165  eirr  11392  odd2np1  11477  n2dvds1  11516  1nprm  11702  structcnvcnv  11881  fvsetsid  11899  0ntop  12080  topnex  12161  bj-nnst  12798  bj-nvel  12929  pwle2  13027  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator