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  1556  nexr  1716  ru  3004  neldifsn  3774  nvel  4193  nlim0  4459  snnex  4513  onprc  4618  dtruex  4625  ordsoexmid  4628  nprrel  4738  0xp  4773  iprc  4966  son2lpi  5098  nfunv  5323  0fv  5635  canth  5920  acexmidlema  5958  acexmidlemb  5959  acexmidlemab  5961  mpo0  6038  php5dom  6985  1ndom2  6987  fi0  7103  pw1ne1  7375  pw1ne3  7376  sucpw1nel3  7379  3nelsucpw1  7380  0nnq  7512  0npr  7631  1ne0sr  7914  pnfnre  8149  mnfnre  8150  ine0  8501  inelr  8692  nn0nepnf  9401  1nuz2  9762  0nrp  9846  inftonninf  10624  lsw0  11078  eirr  12205  odd2np1  12299  n2dvds1  12338  1nprm  12551  structcnvcnv  12963  fvsetsid  12981  fnpr2ob  13287  0g0  13323  0ntop  14594  topnex  14673  umgredgnlp  15856  bj-nvel  16032  pwle2  16137  exmidsbthrlem  16163  trirec0xor  16186