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