Axiom ax-3 5

Description: Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It swaps or transposes the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This axiom is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103).

Assertion

Ref	Expression
ax-3	⊢ ((¬ φ → ¬ ψ) → (ψ → φ))

Detailed syntax breakdown of Axiom ax-3

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff φ
2	1	wn 1	. . 3 wff ¬ φ
3		wps	. . . 4 wff ψ
4	3	wn 1	. . 3 wff ¬ ψ
5	2, 4	wi 2	. 2 wff (¬ φ → ¬ ψ)
6	3, 1	wi 2	. 2 wff (ψ → φ)
7	5, 6	wi 2	1 wff ((¬ φ → ¬ ψ) → (ψ → φ))

This axiom is referenced by:  a3i 69  a3d 70  biigb 129  pm4.1 143  meredith 644  limsuclem 2360

metamath.org