Theorem mto 663

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 640	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 615  ax-in2 616

This theorem is referenced by:  mtbi  671  pm3.2ni  814  pm5.16  829  intnan  930  intnanr  931  equidqe  1546  nexr  1706  ru  2988  neldifsn  3752  nvel  4166  nlim0  4429  snnex  4483  onprc  4588  dtruex  4595  ordsoexmid  4598  nprrel  4708  0xp  4743  iprc  4934  son2lpi  5066  nfunv  5291  0fv  5594  canth  5875  acexmidlema  5913  acexmidlemb  5914  acexmidlemab  5916  mpo0  5992  php5dom  6924  fi0  7041  pw1ne1  7296  pw1ne3  7297  sucpw1nel3  7300  3nelsucpw1  7301  0nnq  7431  0npr  7550  1ne0sr  7833  pnfnre  8068  mnfnre  8069  ine0  8420  inelr  8611  nn0nepnf  9320  1nuz2  9680  0nrp  9764  inftonninf  10534  eirr  11944  odd2np1  12038  n2dvds1  12077  1nprm  12282  structcnvcnv  12694  fvsetsid  12712  fnpr2ob  12983  0g0  13019  0ntop  14243  topnex  14322  bj-nvel  15543  pwle2  15643  exmidsbthrlem  15666  trirec0xor  15689