Theorem eqcomd 1472

Description: Deduction from commutative law for class equality.

Hypothesis

Ref	Expression
eqcomd.1	|- (ph -> A = B)

Assertion

Ref	Expression
eqcomd	|- (ph -> B = A)

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 |- (ph -> A = B)
2		eqcom 1469	. 2 |- (A = B <-> B = A)
3	1, 2	sylib 198	1 |- (ph -> B = A)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  eqtr2d 1500  eqtr3d 1501  eqtr4d 1502  syl5req 1512  syl6req 1516  sylan9req 1520  eqeltrrd 1541  eleqtrrd 1543  syl5eleqr 1547  syl6eqelr 1549  dedhb 1906  eqsstr3d 2086  sseqtr4d 2088  uniiunlem 2122  ifbi 2361  ifboth 2365  dedth 2373  dedth2v 2374  dedth3v 2375  dedth4v 2376  elimhyp 2380  elimhyp2v 2381  elimhyp3v 2382  elimhyp4v 2383  elimdhyp 2385  keephyp2v 2387  keephyp3v 2388  disjsn2 2432  unimax 2522  eqbrtrrd 2627  breqtrrd 2631  syl5breqr 2641  syl6eqbrr 2643  class2seteq 2725  opth 2777  reuuniss 2879  reuuniss2 2881  ordsuc 3055  onsucuni2 3081  onnev 3232  fun2ssres 3539  funimass1 3558  funssfv 3720  oprabval4g 4016  foprab2 4103  nneob 4239  eqer 4255  mapdom2 4474  ssenen 4484  pssnn 4513  unblem2 4518  rankuni 4670  alephfp 4872  cfsuc 4887  1idpr 5105  reclem3pr 5130  recexsrlem 5184  cnegextlem2 5318  negeu 5327  subdit 5399  le2tri3 5563  receu 5670  infm3lem 6000  infmsup 6015  flval2t 6181  elfz1eqt 6424  fzrevralt 6451  expge0t 6522  expge1t 6524  expsubt 6529  sq01t 6582  discrlem3 6588  sqr2irrlem1 6654  crret 6702  crretOLD 6703  crimt 6704  crimtOLD 6705  reim0t 6711  cjexpt 6752  absdivz 6794  recant 6842  bcnp11t 6903  bcpasc 6907  fsum1ps 6956  fsumsplit 6958  ser1ser0 6986  serzmulc 6996  climrecl 7047  climmullem3 7058  clim2serzt 7070  iserzmulc1 7072  clim2serz 7081  serzf0 7105  ser1f0 7106  isumclim3t 7135  isummulc1ALT 7148  fsum0diag3 7195  efaddlem14 7293  efsubt 7313  reeff1o 7368  sinnegt 7384  cosnegt 7385  infxpidmlem8 7502  subtop 7588  islp2 7688  cnpco 7708  iscncl 7709  cnconst 7719  dfms2 7738  metge0 7760  cnmet 7843  cncfmet 7844  bcthlem20 7952  isgrp 7975  isgrpi 7976  grpidinvlem2 7983  grpinvid2 8007  grpinvf 8014  grplactf1o 8034  ablmul 8068  ring2 8086  nvmtri2 8239  ipcj 8301  sspg 8321  ssps 8323  sspn 8329  nmlno0lem 8385  cnph 8409  ipasslem2 8422  siii 8444  minveclem23 8498  minveclem26 8501  minveclem36 8511  hlipcj 8543  cosh111lem2 8630  efifolem1 8637  efifolem6 8642  hiidge0t 8885  bcseq 8907  pjopt 9175  pjpot 9176  shunss 9252  h1de2 9391  fh1t 9478  fh2t 9479  pjot 9533  pjcj 9546  pjrn 9564  hmopret 9763  adjvalvalt 9777  hmopadjt 9779  hmoplint 9782  idhmop 9822  hmopbdopHIL 9828  nmlnop0ALT 9835  nmopunt 9854  cnvbravalt 9956  kbass3t 9963  pjhmop 9984  pjhmopidm 10020  hstoht 10069  sto2 10074  atom1d 10188  atcv0eq 10214  atcv1t 10215  moec 10357  fine2 10375  cdrci 10381  bsi 10382  hmphsyma 10415  hmeogrp 10425  oefil2 10441  cnfilca 10451  mslb1 10473  2wsms 10474  trran 10480  dcsda 10510  1ded 10515  rcmob 10526  1cat 10536  cmpassoh 10573  homgrf 10574  imonclem 10583  cmpmon 10585  icmpmon 10587  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain