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  2471  abid2f  2515  eqnetrri  2536  neeqtrri  2540  eqsstr3i  3303  sseqtr4i  3305  syl5eqssr  3317  syl6sseqr  3319  inrab2  3529  pw1eqadj  4333  nnsucelrlem3  4427  nulge  4457  ltfinirr  4458  ltfinp1  4463  lefinlteq  4464  lefinrflx  4468  ncfinprop  4475  0ceven  4506  eqbrtrri  4661  breqtrri  4665  syl6breqr  4680  cnvresid  5167  fores  5279  1st2nd2  5517  fnfullfun  5859  clos1basesuc  5883  ncaddccl  6145  ce0t  6233  nchoicelem9  6298  nchoicelem19  6308