erbr3b

Description: Biconditional for equivalent elements. (Contributed by Thierry Arnoux, 6-Jan-2020)

		Ref	Expression
	Assertion	erbr3b	$⊢ (R Er X \land A R B) \to (A R C \leftrightarrow B R C)$

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((R Er X \land A R B) \land A R C) \to R Er X$
2		simplr	$⊢ ((R Er X \land A R B) \land A R C) \to A R B$
3		simpr	$⊢ ((R Er X \land A R B) \land A R C) \to A R C$
4	1 2 3	ertr3d	$⊢ ((R Er X \land A R B) \land A R C) \to B R C$
5		simpll	$⊢ ((R Er X \land A R B) \land B R C) \to R Er X$
6		simplr	$⊢ ((R Er X \land A R B) \land B R C) \to A R B$
7		simpr	$⊢ ((R Er X \land A R B) \land B R C) \to B R C$
8	5 6 7	ertrd	$⊢ ((R Er X \land A R B) \land B R C) \to A R C$
9	4 8	impbida	$⊢ (R Er X \land A R B) \to (A R C \leftrightarrow B R C)$

Metamath Proof Explorer