Theorem ersymb

Description: An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	ersymb.1	|- ( ph -> R Er X )
Assertion	ersymb	|- ( ph -> ( A R B <-> B R A ) )

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	|- ( ph -> R Er X )
2	1	adantr	|- ( ( ph /\ A R B ) -> R Er X )
3		simpr	|- ( ( ph /\ A R B ) -> A R B )
4	2 3	ersym	|- ( ( ph /\ A R B ) -> B R A )
5	1	adantr	|- ( ( ph /\ B R A ) -> R Er X )
6		simpr	|- ( ( ph /\ B R A ) -> B R A )
7	5 6	ersym	|- ( ( ph /\ B R A ) -> A R B )
8	4 7	impbida	|- ( ph -> ( A R B <-> B R A ) )