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-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:  eqtr2d  2386  eqtr3d  2387  eqtr4d  2388  syl5req  2398  syl6req  2402  sylan9req  2406  eqeltrrd  2428  eleqtrrd  2430  syl5eleqr  2440  syl6eqelr  2442  eqnetrrd  2537  neeqtrrd  2541  dedhb  3007  eqsstr3d  3307  sseqtr4d  3309  syl6eqssr  3323  dfrab3ss  3534  uneqdifeq  3639  ifbi  3680  ifbothda  3693  dedth  3704  elimhyp  3711  elimhyp2v  3712  elimhyp3v  3713  elimhyp4v  3714  elimdhyp  3716  keephyp2v  3718  keephyp3v  3719  disjsn2  3788  diftpsn3  3850  unimax  3926  iununi  4051  pwadjoin  4120  iotaex  4357  iota4  4358  vfinspsslem1  4551  vfinspss  4552  phi11lem1  4596  eqbrtrrd  4662  breqtrrd  4666  syl5breqr  4676  syl6eqbrr  4678  opeliunxp  4821  fun2ssres  5146  funimass1  5170  funssfv  5344  fnimapr  5375  fvun  5379  f1oiso2  5501  brtxp  5784  brfns  5834  fnpprod  5844  eqer  5962  uniqs  5985  enadj  6061  nchoicelem1  6290