Theorem mto 666

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

Step	Hyp	Ref	Expression
1		mto.2	. 2 |- ( ph -> ps )
2		mto.1	. . 3 |- -. ps
3	2	a1i 9	. 2 |- ( ph -> -. ps )
4	1, 3	pm2.65i 642	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 617  ax-in2 618

This theorem is referenced by:  mtbi  674  pm3.2ni  818  pm5.16  833  intnan  934  intnanr  935  equidqe  1578  nexr  1738  ru  3027  neldifsn  3798  nvel  4217  nlim0  4485  snnex  4539  onprc  4644  dtruex  4651  ordsoexmid  4654  nprrel  4764  0xp  4799  iprc  4993  son2lpi  5125  nfunv  5351  0fv  5665  canth  5952  acexmidlema  5992  acexmidlemb  5993  acexmidlemab  5995  mpo0  6074  php5dom  7024  1ndom2  7026  fi0  7142  pw1ne1  7414  pw1ne3  7415  sucpw1nel3  7418  3nelsucpw1  7419  0nnq  7551  0npr  7670  1ne0sr  7953  pnfnre  8188  mnfnre  8189  ine0  8540  inelr  8731  nn0nepnf  9440  1nuz2  9801  0nrp  9885  inftonninf  10664  lsw0  11119  eirr  12290  odd2np1  12384  n2dvds1  12423  1nprm  12636  structcnvcnv  13048  fvsetsid  13066  fnpr2ob  13373  0g0  13409  0ntop  14681  topnex  14760  umgredgnlp  15950  bj-nvel  16260  pwle2  16364  exmidsbthrlem  16390  trirec0xor  16413