Theorem bj-nnclav

Description: When F. is substituted for ps , this formula is the Clavius law with a doubly negated consequent, which is therefore a minimalistic tautology. Notice the non-intuitionistic proof from peirce and pm2.27 chained using syl . (Contributed by BJ, 4-Dec-2023)

	Ref	Expression
Assertion	bj-nnclav	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜑 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
2	1	a2i	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜑 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )