Theorem erbr3b

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

	Ref	Expression
Assertion	erbr3b	|- ( ( R Er X /\ A R B ) -> ( A R C <-> B R C ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( R Er X /\ A R B ) /\ A R C ) -> R Er X )
2		simplr	|- ( ( ( R Er X /\ A R B ) /\ A R C ) -> A R B )
3		simpr	|- ( ( ( R Er X /\ A R B ) /\ A R C ) -> A R C )
4	1 2 3	ertr3d	|- ( ( ( R Er X /\ A R B ) /\ A R C ) -> B R C )
5		simpll	|- ( ( ( R Er X /\ A R B ) /\ B R C ) -> R Er X )
6		simplr	|- ( ( ( R Er X /\ A R B ) /\ B R C ) -> A R B )
7		simpr	|- ( ( ( R Er X /\ A R B ) /\ B R C ) -> B R C )
8	5 6 7	ertrd	|- ( ( ( R Er X /\ A R B ) /\ B R C ) -> A R C )
9	4 8	impbida	|- ( ( R Er X /\ A R B ) -> ( A R C <-> B R C ) )