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	$$⊢\left(\left(\phi \to \psi \right)\to \phi \right)\to \left(\left(\phi \to \psi \right)\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\left(\phi \to \psi \right)\to \left(\phi \to \psi \right)$$
2	1	a2i	$$⊢\left(\left(\phi \to \psi \right)\to \phi \right)\to \left(\left(\phi \to \psi \right)\to \psi \right)$$