Theorem eqcomi 2357

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ A = B

Assertion

Ref	Expression
eqcomi	⊢ B = A

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ A = B
2		eqcom 2355	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	mpbi 199	1 ⊢ B = A

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-cleq 2346

This theorem is referenced by:  eqtr2i  2374  eqtr3i  2375  eqtr4i  2376  syl5eqr  2399  syl5reqr  2400  syl6eqr  2403  syl6reqr  2404  eqeltrri  2424  eleqtrri  2426  syl5eqelr  2438  syl6eleqr  2444  abid2  2470  abid2f  2514  eqnetrri  2535  neeqtrri  2539  eqsstr3i  3302  sseqtr4i  3304  syl5eqssr  3316  syl6sseqr  3318  inrab2  3528  pw1eqadj  4332  nnsucelrlem3  4426  nulge  4456  ltfinirr  4457  ltfinp1  4462  lefinlteq  4463  lefinrflx  4467  ncfinprop  4474  0ceven  4505  eqbrtrri  4660  breqtrri  4664  syl6breqr  4679  cnvresid  5166  fores  5278  1st2nd2  5516  fnfullfun  5858  clos1basesuc  5882  ncaddccl  6144  ce0t  6232  nchoicelem9  6297  nchoicelem19  6307