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	|- ( ( ( ph -> ps ) -> ph ) -> ( ( ph -> ps ) -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	a2i	|- ( ( ( ph -> ps ) -> ph ) -> ( ( ph -> ps ) -> ps ) )