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  814  intnan  915  intnanr  916  equidqe  1512  nexr  1672  ru  2936  neldifsn  3691  nvel  4100  nlim0  4357  snnex  4411  onprc  4514  dtruex  4521  ordsoexmid  4524  nprrel  4634  0xp  4669  iprc  4857  son2lpi  4985  nfunv  5206  0fv  5506  canth  5781  acexmidlema  5818  acexmidlemb  5819  acexmidlemab  5821  mpo0  5894  php5dom  6811  fi0  6922  pw1ne1  7167  pw1ne3  7168  sucpw1nel3  7171  3nelsucpw1  7172  0nnq  7287  0npr  7406  1ne0sr  7689  pnfnre  7922  mnfnre  7923  ine0  8274  inelr  8464  nn0nepnf  9167  1nuz2  9523  0nrp  9603  inftonninf  10350  eirr  11687  odd2np1  11777  n2dvds1  11816  1nprm  12007  structcnvcnv  12302  fvsetsid  12320  0ntop  12501  topnex  12582  bj-nnst  13428  bj-nvel  13569  pwle2  13667  exmidsbthrlem  13690  trirec0xor  13713