Theorem mto 652

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 629	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 604  ax-in2 605

This theorem is referenced by:  mtbi  660  pm3.2ni  803  pm5.16  818  intnan  919  intnanr  920  equidqe  1520  nexr  1680  ru  2950  neldifsn  3706  nvel  4115  nlim0  4372  snnex  4426  onprc  4529  dtruex  4536  ordsoexmid  4539  nprrel  4649  0xp  4684  iprc  4872  son2lpi  5000  nfunv  5221  0fv  5521  canth  5796  acexmidlema  5833  acexmidlemb  5834  acexmidlemab  5836  mpo0  5912  php5dom  6829  fi0  6940  pw1ne1  7185  pw1ne3  7186  sucpw1nel3  7189  3nelsucpw1  7190  0nnq  7305  0npr  7424  1ne0sr  7707  pnfnre  7940  mnfnre  7941  ine0  8292  inelr  8482  nn0nepnf  9185  1nuz2  9544  0nrp  9625  inftonninf  10376  eirr  11719  odd2np1  11810  n2dvds1  11849  1nprm  12046  structcnvcnv  12410  fvsetsid  12428  0g0  12607  0ntop  12645  topnex  12726  bj-nvel  13779  pwle2  13878  exmidsbthrlem  13901  trirec0xor  13924