Theorem erbr3b

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

	Ref	Expression
Assertion	erbr3b	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝐶 ) → 𝑅 Er 𝑋 )
2		simplr	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝐶 ) → 𝐴 𝑅 𝐵 )
3		simpr	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )
4	1 2 3	ertr3d	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝐶 ) → 𝐵 𝑅 𝐶 )
5		simpll	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝐶 ) → 𝑅 Er 𝑋 )
6		simplr	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐵 )
7		simpr	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝐶 ) → 𝐵 𝑅 𝐶 )
8	5 6 7	ertrd	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )
9	4 8	impbida	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )