Theorem mto 651

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 628	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 603  ax-in2 604

This theorem is referenced by:  mtbi  659  pm3.2ni  802  pm5.16  813  intnan  914  intnanr  915  equidqe  1512  nexr  1670  ru  2903  neldifsn  3648  nvel  4056  nlim0  4311  snnex  4364  onprc  4462  dtruex  4469  ordsoexmid  4472  nprrel  4579  0xp  4614  iprc  4802  son2lpi  4930  nfunv  5151  0fv  5449  acexmidlema  5758  acexmidlemb  5759  acexmidlemab  5761  mpo0  5834  php5dom  6750  fi0  6856  0nnq  7165  0npr  7284  1ne0sr  7567  pnfnre  7800  mnfnre  7801  ine0  8149  inelr  8339  nn0nepnf  9041  1nuz2  9393  0nrp  9470  inftonninf  10207  eirr  11474  odd2np1  11559  n2dvds1  11598  1nprm  11784  structcnvcnv  11964  fvsetsid  11982  0ntop  12163  topnex  12244  bj-nnst  12953  bj-nvel  13084  pwle2  13182  exmidsbthrlem  13206