Theorem eqcomd 2027

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 2024	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	sylib 127	1 ⊢ (φ → B = A)

Syntax hints:   → wi 4   = wceq 1228

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-cleq 2015

This theorem is referenced by:  eqtr2d  2055  eqtr3d  2056  eqtr4d  2057  syl5req  2067  syl6req  2071  sylan9req  2075  eqeltrrd  2097  eleqtrrd  2099  syl5eleqr  2109  syl6eqelr  2111  eqnetrrd  2209  neeqtrrd  2213  dedhb  2687  eqsstr3d  2957  sseqtr4d  2959  syl6eqssr  2973  dfrab3ss  3192  uneqdifeqim  3285  disjsn2  3407  diftpsn3  3479  dfopg  3521  unimax  3588  sndisj  3734  eqbrtrrd  3760  breqtrrd  3764  syl5breqr  3774  syl6eqbrr  3776  class2seteq  3890  opth1  3947  euotd  3965  opelopabsb  3971  tfisi  4237  0nelxp  4299  opeliunxp  4322  euiotaex  4810  iota4  4812  fun2ssres  4869  funimass1  4902  funssfv  5124  fnimapr  5158  fvun1  5164  fmptco  5255  foeqcnvco  5355  f1eqcocnv  5356  f1oiso2  5391  riotass2  5418  riotass  5419  f1ocnvfv3  5425  caovlem2d  5616  f1opw2  5629  sbcopeq1a  5736  csbopeq1a  5737  eloprabi  5745  cnvf1olem  5768  f2ndf  5770  smoiso  5839  nnaword  5995  eqer  6049  uniqs  6075  enq0sym  6287  enq0tr  6289  recexsrlem  6520  cnegexlem2  6780  nnpcan  6826  subdi  6974