Theorem eqcomd 1487

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 1484	. 2 |- (A = B <-> B = A)
3	1, 2	sylib 198	1 |- (ph -> B = A)

Syntax hints:   -> wi 3   = wceq 960

This theorem is referenced by:  eqtr2d 1515  eqtr3d 1516  eqtr4d 1517  syl5req 1527  syl6req 1531  sylan9req 1535  eqeltrrd 1556  eleqtrrd 1558  syl5eleqr 1562  syl6eqelr 1564  dedhb 1922  eqsstr3d 2107  sseqtr4d 2109  uniiunlem 2143  ifbi 2383  ifboth 2387  dedth 2395  dedth2v 2396  dedth3v 2397  dedth4v 2398  elimhyp 2402  elimhyp2v 2403  elimhyp3v 2404  elimhyp4v 2405  elimdhyp 2407  keephyp2v 2409  keephyp3v 2410  disjsn2 2454  unimax 2546  eqbrtrrd 2652  breqtrrd 2656  syl5breqr 2666  syl6eqbrr 2668  class2seteq 2750  opth 2803  reuuniss 2905  reuuniss2 2907  ordsuc 3081  onsucuni2 3107  onnev 3258  fun2ssres 3569  funimass1 3588  funssfv 3751  oprabval4g 4047  foprab2 4135  nneob 4271  eqer 4287  mapdom2 4514  ssenen 4524  pssnn 4554  unblem2 4559  rankuni 4715  cardsucinf 4861  alephfp 4920  cfsuc 4935  1idpr 5153  reclem3pr 5178  recexsrlem 5232  cnegexlem2 5366  negeui 5375  subdi 5447  le2tri3i 5609  receui 5721  infm3lem 6085  infmsup 6100  flval2 6298  modcyc 6321  elfz1eq 6460  fzrevral 6487  expge0 6622  expge1 6624  expsub 6629  sq01 6682  discrlem3 6690  sqr2irrlem1 6756  crre 6801  crim 6802  reim0 6806  cjexp 6849  absdivzi 6891  recan 6937  bcnp11 6997  bcpasci 7001  fsum1ps 7050  fsumspli 7052  ser1ser0i 7080  serzmulci 7090  climrecli 7142  climmullem3 7154  clim2serzti 7166  iserzmulc1i 7168  clim2serzi 7177  serzf0i 7201  ser1f0i 7202  isumclim3ti 7232  isummulc1iALT 7245  fsum0diag3 7292  efaddlem14 7383  efsub 7403  reeff1o 7458  sinneg 7474  cosneg 7475  infxpidmlem8 7592  subtop 7674  islp2 7773  cnpco 7795  iscncl 7796  cnconst 7806  dfms2 7825  metge0 7845  cnmet 7930  cncfmet 7931  bcthlem20 8044  isgrp 8067  isgrpi 8068  grpidinvlem2 8075  grpinvid2 8098  grpinvf 8104  grplactf1o 8123  ablmul 8156  ring2 8174  nvmtri2 8325  ipcj 8392  sspg 8412  ssps 8414  sspn 8420  nmlno0lem 8478  cnph 8503  ipasslem2 8516  siii 8538  minveclem23 8592  minveclem26 8595  minveclem36 8605  hlipcj 8638  abssinper 8736  cosh111lem2 8739  efifolem1 8746  efifolem6 8751  hiidge0 8988  bcseqi 9010  pjop 9284  pjpo 9285  shunssi 9361  h1de2i 9500  fh1 9585  fh2 9586  pjo 9640  pjcji 9653  pjrni 9671  hmopre 9871  adjvalval 9885  hmopadj 9887  hmoplin 9890  idhmop 9930  hmopbdopiHIL 9936  nmlnop0iALT 9944  nmopun 9963  cnvbraval 10067  bracnlnval 10071  kbass3 10075  pjhmopi 10097  pjhmopidm 10134  hstoh 10184  sto2i 10189  atom1d 10305  atcv0eq 10331  atcv1 10332  moec 10481  domrngref 10499  domfldref 10500  fine2 10511  cdrci 10527  bsi 10528  hmphsyma 10561  hmeogrp 10571  set2elt 10578  setwoe 10579  oefil2 10599  cnfilca 10609  rcfpfillem6 10615  mslb1 10650  2wsms 10651  trran 10657  dcsda 10687  1ded 10692  rcmob 10703  1cat 10713  cmpassoh 10750  homgrf 10751  imonclem 10762  cmpmon 10764  icmpmon 10765  isfuna 10777  idfisf 10783

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 967  ax-4 977  ax-5o 979  ax-ext 1464

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

Copyright terms: Public domain