Theorem mto 663

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 640	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 615  ax-in2 616

This theorem is referenced by:  mtbi  671  pm3.2ni  814  pm5.16  829  intnan  930  intnanr  931  equidqe  1546  nexr  1706  ru  2988  neldifsn  3753  nvel  4167  nlim0  4430  snnex  4484  onprc  4589  dtruex  4596  ordsoexmid  4599  nprrel  4709  0xp  4744  iprc  4935  son2lpi  5067  nfunv  5292  0fv  5595  canth  5876  acexmidlema  5914  acexmidlemb  5915  acexmidlemab  5917  mpo0  5993  php5dom  6925  fi0  7042  pw1ne1  7298  pw1ne3  7299  sucpw1nel3  7302  3nelsucpw1  7303  0nnq  7433  0npr  7552  1ne0sr  7835  pnfnre  8070  mnfnre  8071  ine0  8422  inelr  8613  nn0nepnf  9322  1nuz2  9682  0nrp  9766  inftonninf  10536  eirr  11946  odd2np1  12040  n2dvds1  12079  1nprm  12292  structcnvcnv  12704  fvsetsid  12722  fnpr2ob  12993  0g0  13029  0ntop  14253  topnex  14332  bj-nvel  15553  pwle2  15653  exmidsbthrlem  15676  trirec0xor  15699