Axiom ax-3

Description: AxiomTransp. 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 calledTransp or "the principle of transposition" inPrincipia Mathematica (Theorem *2.17 of WhiteheadRussell p. 103). We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. (Contributed by NM, 30-Sep-1992) Use its alias con4 instead. (New usage is discouraged.)

	Ref	Expression
Assertion	ax-3	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( 𝜓 → 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1	0	wn	⊢ ¬ 𝜑
2		wps	⊢ 𝜓
3	2	wn	⊢ ¬ 𝜓
4	1 3	wi	⊢ ( ¬ 𝜑 → ¬ 𝜓 )
5	2 0	wi	⊢ ( 𝜓 → 𝜑 )
6	4 5	wi	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( 𝜓 → 𝜑 ) )