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

Metamath Proof Explorer

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 𝑋 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )