Metamath Proof Explorer

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