Theorem clav-P1.12 68

Description: Clavious's Law.

The other form is nclav-P1.14 73.

Assertion

Ref	Expression
clav-P1.12	⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Proof of Theorem clav-P1.12

Step	Hyp	Ref	Expression
1		poe-P1.11a 65	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → ¬ (¬ 𝜑 → 𝜑)))
2	1	axL2.SH 31	. . 3 ⊢ ((¬ 𝜑 → 𝜑) → (¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑)))
3	2	axL3.AC.SH 47	. 2 ⊢ ((¬ 𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑))
4	3	rae-P1.5.SH 38	1 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Syntax hints:  ¬ wff-neg 9   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem is referenced by:  clav-P1.12.AC.SH  69  clav-P1.12.2AC.SH  70  dneg-P1.13a  71  nclav-P1.14  73