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	⊢ ¬ 𝜓
mto.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mto	⊢ ¬ 𝜑

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.2	. 2 ⊢ (𝜑 → 𝜓)
2		mto.1	. . 3 ⊢ ¬ 𝜓
3	2	a1i 9	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	1, 3	pm2.65i 644	1 ⊢ ¬ 𝜑

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  3041  neldifsn  3823  nvel  4243  nlim0  4515  snnex  4569  onprc  4674  dtruex  4681  ordsoexmid  4684  nprrel  4795  0xp  4830  iprc  5026  son2lpi  5159  nfunv  5385  0fv  5708  canth  6001  acexmidlema  6041  acexmidlemb  6042  acexmidlemab  6044  mpo0  6123  php5dom  7117  1ndom2  7119  fi0  7262  pw1ne1  7539  pw1ne3  7540  sucpw1nel3  7543  3nelsucpw1  7544  0nnq  7679  0npr  7798  1ne0sr  8081  pnfnre  8315  mnfnre  8316  ine0  8667  inelr  8858  nn0nepnf  9571  1nuz2  9938  0nrp  10022  inftonninf  10804  lsw0  11272  eirr  12465  odd2np1  12559  n2dvds1  12598  1nprm  12811  ballotfilem2  13142  structcnvcnv  13228  fvsetsid  13246  fnpr2ob  13553  0g0  13589  0ntop  14872  topnex  14951  umgredgnlp  16147  konigsberg  16488  bj-nvel  16667  pw1ninf  16765  pwle2  16772  exmidsbthrlem  16802  trirec0xor  16829