Axiom ax-L3 13

Description: Axiom of Transposition.

Assertion

Ref	Expression
ax-L3	⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

Detailed syntax breakdown of Axiom ax-L3

Step	Hyp	Ref	Expression
1		wff-ph	. . . 4 wff 𝜑
2	1	wff-neg 9	. . 3 wff ¬ 𝜑
3		wff-ps	. . . 4 wff 𝜓
4	3	wff-neg 9	. . 3 wff ¬ 𝜓
5	2, 4	wff-imp 10	. 2 wff (¬ 𝜑 → ¬ 𝜓)
6	3, 1	wff-imp 10	. 2 wff (𝜓 → 𝜑)
7	5, 6	wff-imp 10	1 wff ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

This axiom is referenced by:  axL3.SH  32  axL3.AC.SH  47  poe-P1.11a  65  trnsp-P1.15a  76  trnsp-P1.15b  78  trnsp-P1.15d  83