letri3

		Ref	Expression
	Assertion	letri3	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$

Step	Hyp	Ref	Expression
1		lttri3	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (\neg A < B \land \neg B < A))$
2	1	biancomd	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (\neg B < A \land \neg A < B))$
3		lenlt	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow \neg B < A)$
4		lenlt	$⊢ (B \in ℝ \land A \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
5	4	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
6	3 5	anbi12d	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \leq B \land B \leq A) \leftrightarrow (\neg B < A \land \neg A < B))$
7	2 6	bitr4d	$⊢ (A \in ℝ \land B \in ℝ) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$

Metamath Proof Explorer