Theorem nclav-P1.14 73

Description: Negated Clavius's Law.

This is the negated form of clav-P1.12 68.

Assertion

Ref	Expression
nclav-P1.14	⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)

Proof of Theorem nclav-P1.14

Step	Hyp	Ref	Expression
1		dneg-P1.13a 71	. . 3 ⊢ (¬ ¬ 𝜑 → 𝜑)
2	1	imsubl-P1.7b.SH 55	. 2 ⊢ ((𝜑 → ¬ 𝜑) → (¬ ¬ 𝜑 → ¬ 𝜑))
3		clav-P1.12 68	. 2 ⊢ ((¬ ¬ 𝜑 → ¬ 𝜑) → ¬ 𝜑)
4	2, 3	syl-P1.2 34	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.14.AC.SH  74  nclav-P1.14.2AC.SH  75