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 
|- ( ( 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 ) )