Theorem con3 86

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

Assertion

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

Proof of Theorem con3

Step	Hyp	Ref	Expression
1		negb 79	. . 3 ⊢ (ψ → ¬ ¬ ψ)
2	1	syl3 18	. 2 ⊢ ((φ → ψ) → (φ → ¬ ¬ ψ))
3	2	con2d 83	1 ⊢ ((φ → ψ) → (¬ ψ → ¬ φ))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  con3d 87  impt 122  pm4.1 143  jao 274  mtt 534  pclem6 555  meredith 644  hbnt 710  19.22 722  tfinds 2401  inf3lem2 3465  climunii 4883  hlimunii 5143

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

metamath.org