Theorem mto 93

Description: The rule of modus tollens.

Hypotheses

Ref	Expression
mto.1	⊢ ¬ ψ
mto.2	⊢ (φ → ψ)

Assertion

Ref	Expression
mto	⊢ ¬ φ

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.1	. 2 ⊢ ¬ ψ
2		mto.2	. . 3 ⊢ (φ → ψ)
3	2	con3i 90	. 2 ⊢ (¬ ψ → ¬ φ)
4	1, 3	ax-mp 6	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  intnan 516  intnanr 517  ru 1437  pssn2lp 1571  onprc 2240  ordeleqon 2241  onuninsuc 2356  orduninsuc 2365  snsn0non 2371  xp0r 2474  0nelxp 2475  son2lpi 2631  nfunv 2693  tz7.44lem1 2965  tz7.44-2 2967  0nelqs 3234  canth2 3381  rankpw 3528  kmlem16 3595  cardprc 3667  alephprc 3698  cfsuc 3709  nd1 3732  nd2 3733  1pr 3911  1ne0sr 3999  recgt0i 4385  nnunb 4520  ine0 4524  inelr 4527  halfnz 4586  indstr 4611  nneo 4719  sqr2irr 4782  ruclem36 4920  ruclem37 4921  ruc 4924

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org