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  5667  canth  5958  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  mpo0  6080  php5dom  7032  1ndom2  7034  fi0  7153  pw1ne1  7425  pw1ne3  7426  sucpw1nel3  7429  3nelsucpw1  7430  0nnq  7562  0npr  7681  1ne0sr  7964  pnfnre  8199  mnfnre  8200  ine0  8551  inelr  8742  nn0nepnf  9451  1nuz2  9813  0nrp  9897  inftonninf  10676  lsw0  11132  eirr  12306  odd2np1  12400  n2dvds1  12439  1nprm  12652  structcnvcnv  13064  fvsetsid  13082  fnpr2ob  13389  0g0  13425  0ntop  14697  topnex  14776  umgredgnlp  15966  bj-nvel  16343  pw1ninf  16442  pwle2  16451  exmidsbthrlem  16478  trirec0xor  16501