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  7168  1ndom2  7170  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  9649  1nuz2  10022  0nrp  10107  inftonninf  10900  lsw0  11374  eirr  12571  odd2np1  12665  n2dvds1  12704  1nprm  12917  ballotfilem2  13286  structcnvcnv  13426  fvsetsid  13444  fnpr2ob  13720  0g0  13755  0ntop  15233  topnex  15312  umgredgnlp  16598  konigsberg  16939  bj-nvel  17128  pw1ninf  17226  pwle2  17233  wexmiddifxylem  17250  exmidsbthrlem  17273  trirec0xor  17301  alseu-no-surprise  17386