Theorem mto 668

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 644	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 619  ax-in2 620

This theorem is referenced by:  mtbi  676  pm3.2ni  820  pm5.16  835  intnan  936  intnanr  937  equidqe  1580  nexr  1740  ru  3030  neldifsn  3803  nvel  4222  nlim0  4491  snnex  4545  onprc  4650  dtruex  4657  ordsoexmid  4660  nprrel  4771  0xp  4806  iprc  5001  son2lpi  5133  nfunv  5359  0fv  5677  canth  5969  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  mpo0  6091  php5dom  7049  1ndom2  7051  fi0  7174  pw1ne1  7447  pw1ne3  7448  sucpw1nel3  7451  3nelsucpw1  7452  0nnq  7584  0npr  7703  1ne0sr  7986  pnfnre  8221  mnfnre  8222  ine0  8573  inelr  8764  nn0nepnf  9473  1nuz2  9840  0nrp  9924  inftonninf  10705  lsw0  11165  eirr  12358  odd2np1  12452  n2dvds1  12491  1nprm  12704  structcnvcnv  13116  fvsetsid  13134  fnpr2ob  13441  0g0  13477  0ntop  14750  topnex  14829  umgredgnlp  16022  konigsberg  16363  bj-nvel  16543  pw1ninf  16641  pwle2  16650  exmidsbthrlem  16677  trirec0xor  16700