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  1543  nexr  1703  ru  2985  neldifsn  3749  nvel  4163  nlim0  4426  snnex  4480  onprc  4585  dtruex  4592  ordsoexmid  4595  nprrel  4705  0xp  4740  iprc  4931  son2lpi  5063  nfunv  5288  0fv  5591  canth  5872  acexmidlema  5910  acexmidlemb  5911  acexmidlemab  5913  mpo0  5989  php5dom  6921  fi0  7036  pw1ne1  7291  pw1ne3  7292  sucpw1nel3  7295  3nelsucpw1  7296  0nnq  7426  0npr  7545  1ne0sr  7828  pnfnre  8063  mnfnre  8064  ine0  8415  inelr  8605  nn0nepnf  9314  1nuz2  9674  0nrp  9758  inftonninf  10516  eirr  11925  odd2np1  12017  n2dvds1  12056  1nprm  12255  structcnvcnv  12637  fvsetsid  12655  fnpr2ob  12926  0g0  12962  0ntop  14186  topnex  14265  bj-nvel  15459  pwle2  15559  exmidsbthrlem  15582  trirec0xor  15605