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  3031  neldifsn  3807  nvel  4227  nlim0  4497  snnex  4551  onprc  4656  dtruex  4663  ordsoexmid  4666  nprrel  4777  0xp  4812  iprc  5007  son2lpi  5140  nfunv  5366  0fv  5686  canth  5979  acexmidlema  6019  acexmidlemb  6020  acexmidlemab  6022  mpo0  6101  php5dom  7092  1ndom2  7094  fi0  7234  pw1ne1  7507  pw1ne3  7508  sucpw1nel3  7511  3nelsucpw1  7512  0nnq  7644  0npr  7763  1ne0sr  8046  pnfnre  8280  mnfnre  8281  ine0  8632  inelr  8823  nn0nepnf  9534  1nuz2  9901  0nrp  9985  inftonninf  10767  lsw0  11227  eirr  12420  odd2np1  12514  n2dvds1  12553  1nprm  12766  structcnvcnv  13178  fvsetsid  13196  fnpr2ob  13503  0g0  13539  0ntop  14818  topnex  14897  umgredgnlp  16093  konigsberg  16434  bj-nvel  16613  pw1ninf  16711  pwle2  16720  exmidsbthrlem  16750  trirec0xor  16777