Theorem mto 668

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 644	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 619  ax-in2 620

This theorem is referenced by:  mtbi  677  pm3.2ni  821  pm5.16  836  intnan  937  intnanr  938  equidqe  1581  nexr  1740  ru  3040  neldifsn  3822  nvel  4242  nlim0  4514  snnex  4568  onprc  4673  dtruex  4680  ordsoexmid  4683  nprrel  4794  0xp  4829  iprc  5025  son2lpi  5158  nfunv  5384  0fv  5707  canth  6000  acexmidlema  6040  acexmidlemb  6041  acexmidlemab  6043  mpo0  6122  php5dom  7116  1ndom2  7118  fi0  7261  pw1ne1  7538  pw1ne3  7539  sucpw1nel3  7542  3nelsucpw1  7543  0nnq  7678  0npr  7797  1ne0sr  8080  pnfnre  8314  mnfnre  8315  ine0  8666  inelr  8857  nn0nepnf  9570  1nuz2  9937  0nrp  10021  inftonninf  10803  lsw0  11268  eirr  12461  odd2np1  12555  n2dvds1  12594  1nprm  12807  structcnvcnv  13220  fvsetsid  13238  fnpr2ob  13545  0g0  13581  0ntop  14864  topnex  14943  umgredgnlp  16139  konigsberg  16480  bj-nvel  16659  pw1ninf  16757  pwle2  16764  exmidsbthrlem  16794  trirec0xor  16821