Metamath Proof Explorer


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 φRErX
Assertion ersymb φARBBRA

Proof

Step Hyp Ref Expression
1 ersymb.1 φRErX
2 1 adantr φARBRErX
3 simpr φARBARB
4 2 3 ersym φARBBRA
5 1 adantr φBRARErX
6 simpr φBRABRA
7 5 6 ersym φBRAARB
8 4 7 impbida φARBBRA