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  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  7217  pw1ne1  7490  pw1ne3  7491  sucpw1nel3  7494  3nelsucpw1  7495  0nnq  7627  0npr  7746  1ne0sr  8029  pnfnre  8263  mnfnre  8264  ine0  8615  inelr  8806  nn0nepnf  9517  1nuz2  9884  0nrp  9968  inftonninf  10750  lsw0  11210  eirr  12403  odd2np1  12497  n2dvds1  12536  1nprm  12749  structcnvcnv  13161  fvsetsid  13179  fnpr2ob  13486  0g0  13522  0ntop  14801  topnex  14880  umgredgnlp  16076  konigsberg  16417  bj-nvel  16596  pw1ninf  16694  pwle2  16703  exmidsbthrlem  16733  trirec0xor  16760