Theorem simprimi

Description: Inference associated with simprim . Proved exactly as step 11 is obtained from step 4 in dfbi1ALTa . (Contributed by Eric Schmidt, 22-Oct-2025) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	simprimi.1	$$⊢\neg \left(\phi \to \neg \psi \right)$$
Assertion	simprimi	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		simprimi.1	$$⊢\neg \left(\phi \to \neg \psi \right)$$
2		tru	$$⊢\top$$
3		ax-1	$$⊢\neg \psi \to \left(\phi \to \neg \psi \right)$$
4	1	a1i	$$⊢\neg \neg \top \to \neg \left(\phi \to \neg \psi \right)$$
5	4	con4i	$$⊢\left(\phi \to \neg \psi \right)\to \neg \top$$
6	5	a1i	$$⊢\neg \psi \to \left(\left(\phi \to \neg \psi \right)\to \neg \top \right)$$
7	6	a2i	$$⊢\left(\neg \psi \to \left(\phi \to \neg \psi \right)\right)\to \left(\neg \psi \to \neg \top \right)$$
8	3 7	ax-mp	$$⊢\neg \psi \to \neg \top$$
9	8	con4i	$$⊢\top \to \psi$$
10	2 9	ax-mp	$$⊢\psi$$