Theorem eqcomd 2358

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqcomd	⊢ (φ → B = A)

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 ⊢ (φ → A = B)
2		eqcom 2355	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	sylib 188	1 ⊢ (φ → B = A)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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:  eqtr2d  2386  eqtr3d  2387  eqtr4d  2388  syl5req  2398  syl6req  2402  sylan9req  2406  eqeltrrd  2428  eleqtrrd  2430  syl5eleqr  2440  syl6eqelr  2442  eqnetrrd  2536  neeqtrrd  2540  dedhb  3006  eqsstr3d  3306  sseqtr4d  3308  syl6eqssr  3322  dfrab3ss  3533  uneqdifeq  3638  ifbi  3679  ifbothda  3692  dedth  3703  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elimdhyp  3715  keephyp2v  3717  keephyp3v  3718  disjsn2  3787  diftpsn3  3849  unimax  3925  iununi  4050  pwadjoin  4119  iotaex  4356  iota4  4357  vfinspsslem1  4550  vfinspss  4551  phi11lem1  4595  eqbrtrrd  4661  breqtrrd  4665  syl5breqr  4675  syl6eqbrr  4677  opeliunxp  4820  fun2ssres  5145  funimass1  5169  funssfv  5343  fnimapr  5374  fvun  5378  f1oiso2  5500  brtxp  5783  brfns  5833  fnpprod  5843  eqer  5961  uniqs  5984  enadj  6060  nchoicelem1  6289