Theorem mto 662

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 639	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 614  ax-in2 615

This theorem is referenced by:  mtbi  670  pm3.2ni  813  pm5.16  828  intnan  929  intnanr  930  equidqe  1532  nexr  1692  ru  2962  neldifsn  3723  nvel  4137  nlim0  4395  snnex  4449  onprc  4552  dtruex  4559  ordsoexmid  4562  nprrel  4672  0xp  4707  iprc  4896  son2lpi  5026  nfunv  5250  0fv  5551  canth  5829  acexmidlema  5866  acexmidlemb  5867  acexmidlemab  5869  mpo0  5945  php5dom  6863  fi0  6974  pw1ne1  7228  pw1ne3  7229  sucpw1nel3  7232  3nelsucpw1  7233  0nnq  7363  0npr  7482  1ne0sr  7765  pnfnre  7999  mnfnre  8000  ine0  8351  inelr  8541  nn0nepnf  9247  1nuz2  9606  0nrp  9689  inftonninf  10441  eirr  11786  odd2np1  11878  n2dvds1  11917  1nprm  12114  structcnvcnv  12478  fvsetsid  12496  fnpr2ob  12759  0g0  12795  0ntop  13510  topnex  13589  bj-nvel  14652  pwle2  14751  exmidsbthrlem  14773  trirec0xor  14796