This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ine1

Description: _i is not 1. (Contributed by SN, 25-Apr-2025)

		Ref	Expression
	Assertion	ine1	$⊢ i \neq 1$

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		inelr	$⊢ \neg i \in ℝ$
3		nelne2	$⊢ (1 \in ℝ \land \neg i \in ℝ) \to 1 \neq i$
4	1 2 3	mp2an	$⊢ 1 \neq i$
5	4	necomi	$⊢ i \neq 1$