Theorem con3 94

Description: Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103.

Assertion

Ref	Expression
con3	⊢ ((φ → ψ) → (¬ ψ → ¬ φ))

Proof of Theorem con3

Step	Hyp	Ref	Expression
1		negb 86	. . 3 ⊢ (ψ → ¬ ¬ ψ)
2	1	imim2i 17	. 2 ⊢ ((φ → ψ) → (φ → ¬ ¬ ψ))
3	2	con2d 91	1 ⊢ ((φ → ψ) → (¬ ψ → ¬ φ))

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  con3d 95  impt 141  pm4.1 164  jao 340  mtt 711  pclem6 740  meredith 922  nicodraw 950  ax4 970  hbnt 1000  19.22 1037  ax11indn 1364  ralf0 2355  ivthlem7 7230  ivthlem7OLD 7239  hlimunii 9047

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

Copyright terms: Public domain