Theorem eqvrelsymb

Description: An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 12-Aug-2015) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.)

	Ref	Expression
Hypothesis	eqvrelsymb.1	$$⊢\phi \to EqvRelR$$
Assertion	eqvrelsymb	$$⊢\phi \to \left(ARB\leftrightarrow BRA\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelsymb.1	$$⊢\phi \to EqvRelR$$
2	1	adantr	$$⊢\left(\phi \wedge ARB\right)\to EqvRelR$$
3		simpr	$$⊢\left(\phi \wedge ARB\right)\to ARB$$
4	2 3	eqvrelsym	$$⊢\left(\phi \wedge ARB\right)\to BRA$$
5	1	adantr	$$⊢\left(\phi \wedge BRA\right)\to EqvRelR$$
6		simpr	$$⊢\left(\phi \wedge BRA\right)\to BRA$$
7	5 6	eqvrelsym	$$⊢\left(\phi \wedge BRA\right)\to ARB$$
8	4 7	impbida	$$⊢\phi \to \left(ARB\leftrightarrow BRA\right)$$