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	⊢ ¬ ( 𝜑 → ¬ 𝜓 )
Assertion	simprimi	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		simprimi.1	⊢ ¬ ( 𝜑 → ¬ 𝜓 )
2		tru	⊢ ⊤
3		ax-1	⊢ ( ¬ 𝜓 → ( 𝜑 → ¬ 𝜓 ) )
4	1	a1i	⊢ ( ¬ ¬ ⊤ → ¬ ( 𝜑 → ¬ 𝜓 ) )
5	4	con4i	⊢ ( ( 𝜑 → ¬ 𝜓 ) → ¬ ⊤ )
6	5	a1i	⊢ ( ¬ 𝜓 → ( ( 𝜑 → ¬ 𝜓 ) → ¬ ⊤ ) )
7	6	a2i	⊢ ( ( ¬ 𝜓 → ( 𝜑 → ¬ 𝜓 ) ) → ( ¬ 𝜓 → ¬ ⊤ ) )
8	3 7	ax-mp	⊢ ( ¬ 𝜓 → ¬ ⊤ )
9	8	con4i	⊢ ( ⊤ → 𝜓 )
10	2 9	ax-mp	⊢ 𝜓