Theorem mto 662

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 639	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 614  ax-in2 615

This theorem is referenced by:  mtbi  670  pm3.2ni  813  pm5.16  828  intnan  929  intnanr  930  equidqe  1532  nexr  1692  ru  2963  neldifsn  3724  nvel  4138  nlim0  4396  snnex  4450  onprc  4553  dtruex  4560  ordsoexmid  4563  nprrel  4673  0xp  4708  iprc  4897  son2lpi  5027  nfunv  5251  0fv  5552  canth  5832  acexmidlema  5869  acexmidlemb  5870  acexmidlemab  5872  mpo0  5948  php5dom  6866  fi0  6977  pw1ne1  7231  pw1ne3  7232  sucpw1nel3  7235  3nelsucpw1  7236  0nnq  7366  0npr  7485  1ne0sr  7768  pnfnre  8002  mnfnre  8003  ine0  8354  inelr  8544  nn0nepnf  9250  1nuz2  9609  0nrp  9692  inftonninf  10444  eirr  11789  odd2np1  11881  n2dvds1  11920  1nprm  12117  structcnvcnv  12481  fvsetsid  12499  fnpr2ob  12765  0g0  12801  0ntop  13647  topnex  13726  bj-nvel  14789  pwle2  14889  exmidsbthrlem  14911  trirec0xor  14934