Theorem mto 664

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  672  pm3.2ni  815  pm5.16  830  intnan  931  intnanr  932  equidqe  1555  nexr  1715  ru  2997  neldifsn  3763  nvel  4178  nlim0  4442  snnex  4496  onprc  4601  dtruex  4608  ordsoexmid  4611  nprrel  4721  0xp  4756  iprc  4948  son2lpi  5080  nfunv  5305  0fv  5614  canth  5899  acexmidlema  5937  acexmidlemb  5938  acexmidlemab  5940  mpo0  6017  php5dom  6962  fi0  7079  pw1ne1  7343  pw1ne3  7344  sucpw1nel3  7347  3nelsucpw1  7348  0nnq  7479  0npr  7598  1ne0sr  7881  pnfnre  8116  mnfnre  8117  ine0  8468  inelr  8659  nn0nepnf  9368  1nuz2  9729  0nrp  9813  inftonninf  10589  lsw0  11043  eirr  12123  odd2np1  12217  n2dvds1  12256  1nprm  12469  structcnvcnv  12881  fvsetsid  12899  fnpr2ob  13205  0g0  13241  0ntop  14512  topnex  14591  bj-nvel  15870  pwle2  15972  exmidsbthrlem  15998  trirec0xor  16021