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