Theorem mto 672

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 648	1 |- -. ph

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mtbi  681  pm3.2ni  825  pm5.16  840  intnan  941  intnanr  942  equidqe  1585  nexr  1744  ru  3050  neldifsn  3844  nvel  4268  nlim0  4541  snnex  4596  onprc  4701  dtruex  4708  ordsoexmid  4711  nprrel  4822  0xp  4857  iprc  5053  son2lpi  5187  nfunv  5413  0fv  5737  canth  6039  acexmidlema  6079  acexmidlemb  6080  acexmidlemab  6082  mpo0  6161  php5dom  7170  1ndom2  7172  fi0  7314  pw1ne1  7594  pw1ne3  7595  sucpw1nel3  7598  3nelsucpw1  7599  0nnq  7737  0npr  7856  1ne0sr  8139  pnfnre  8373  mnfnre  8374  ine0  8728  inelr  8920  nn0nepnf  9647  1nuz2  10021  0nrp  10106  inftonninf  10899  lsw0  11373  eirr  12570  odd2np1  12664  n2dvds1  12703  1nprm  12916  ballotfilem2  13285  structcnvcnv  13425  fvsetsid  13443  fnpr2ob  13719  0g0  13754  0ntop  15250  topnex  15329  umgredgnlp  16615  konigsberg  16956  bj-nvel  17145  pw1ninf  17243  pwle2  17250  wexmiddifxylem  17267  exmidsbthrlem  17290  trirec0xor  17318  alseu-no-surprise  17403