Theorem cleqcomd 1106

Description: Deduction from commutative law for class equality.

Hypothesis

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

Assertion

Ref	Expression
cleqcomd	⊢ (φ → B = A)

Proof of Theorem cleqcomd

Step	Hyp	Ref	Expression
1		cleqcomd.1	. 2 ⊢ (φ → A = B)
2		cleqcom 1103	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	sylib 173	1 ⊢ (φ → B = A)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  eqtr2d 1129  eqtr3d 1130  eqtr4d 1131  syl5req 1137  syl6req 1141  eqeltrrd 1164  eleqtrrd 1166  eqsstr3d 1535  sseqtr4d 1537  3sstr4d 1543  ifbi 1783  dedth 1784  dedth2v 1785  dedth3v 1786  elimhyp 1790  elimhyp2v 1791  elimhyp3v 1792  keephyp 1794  keephyp3v 1795  disjsn2 1837  opth 1898  eqbrtrrd 2079  breqtrrd 2083  ordsuc 2318  fun2ssres 2699  funimass1 2712  fndmu 2725  funssfv 2841  fvopabgf 2874  fvopabnf 2875  oprabval4g 3053  mapdom2 3389  mapunen 3397  ssenen 3399  unblem2 3432  rankonid 3538  cfsuc 3709  1idpr 3927  reclem3pr 3952  recexsrlem 4006  axcnre 4087  negeu 4124  receu 4215  le2tri3 4311  nndiv 4453  discrlem3 4715  sqr2irrlem1 4777  infxpidmlem8 4940  infxpidmlem10 4942  hvsubcan2t 5017  hiidrclt 5053  hiidge0t 5056  bcseq 5073  pjopt 5264  pjpot 5265  shscl 5282  shunss 5338  h1de2 5458  pjot 5561  pjcj 5575  pjrn 5587  sto2 5678  atom1d 5750  atcv0eq 5767  atcv1 5768

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org