Theorem mto 106

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 98	. 2 ⊢ (¬ ψ → ¬ φ)
4	1, 3	ax-mp 7	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  intnan 689  intnanr 690  ru 1928  pssn2lp 2137  axnul2 2698  nvel 2704  onprc 2979  ordeleqon 2980  onuninsuc 3098  orduninsuc 3104  snsn0non 3115  nprrel 3199  xp0r 3229  0nelxp 3230  inelv 3346  son2lpi 3430  nfunv 3532  tz7.44lem1 3912  tz7.44-2 3914  0nelqs 4282  sdomn2lp 4455  canth2 4464  2pwuninel 4465  rankpw 4656  rankxplim3 4686  kmlem16 4752  cardprc 4833  alephprc 4865  unialeph 4867  cfsuc 4887  nd1 4910  nd2 4911  1pr 5089  1ne0sr 5177  ine0 5406  pnfnre 5468  mnfnre 5469  pnfnemnf 5509  recgt0i 5770  nnunb 6017  nneo 6144  0nrp 6230  indstr 6393  sqr2irr 6659  inelr 6665  climunii 7035  climubi 7089  ivthlem8 7223  ivthlem8OLD 7232  eirrlem5 7334  ruclem36 7488  ruclem37 7489  ruc 7492  tpsex 7547  0ngrp 7989  vcoprne 8136  sinhalfpilem 8598  dmadjrnb 9747  empntop 10393  emnfil 10440

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

Copyright terms: Public domain