Theorem eqcomd 1480

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  eqtr2d 1508  eqtr3d 1509  eqtr4d 1510  syl5req 1520  syl6req 1524  sylan9req 1528  eqeltrrd 1549  eleqtrrd 1551  syl5eleqr 1555  syl6eqelr 1557  dedhb 1915  eqsstr3d 2096  sseqtr4d 2098  uniiunlem 2132  ifbi 2371  ifboth 2375  dedth 2383  dedth2v 2384  dedth3v 2385  dedth4v 2386  elimhyp 2390  elimhyp2v 2391  elimhyp3v 2392  elimhyp4v 2393  elimdhyp 2395  keephyp2v 2397  keephyp3v 2398  disjsn2 2442  unimax 2532  eqbrtrrd 2637  breqtrrd 2641  syl5breqr 2651  syl6eqbrr 2653  class2seteq 2735  opth 2787  reuuniss 2889  reuuniss2 2891  ordsuc 3065  onsucuni2 3091  onnev 3242  fun2ssres 3553  funimass1 3572  funssfv 3735  oprabval4g 4031  foprab2 4119  nneob 4255  eqer 4271  mapdom2 4494  ssenen 4504  pssnn 4534  unblem2 4541  rankuni 4698  alephfp 4900  cfsuc 4915  1idpr 5133  reclem3pr 5158  recexsrlem 5212  cnegextlem2 5346  negeu 5355  subdit 5427  le2tri3 5589  receu 5701  infm3lem 6053  infmsup 6068  flval2t 6238  quoremOLD 6252  elfz1eqt 6492  fzrevralt 6519  expge0t 6591  expge1t 6593  expsubt 6598  sq01t 6651  discrlem3 6658  sqr2irrlem1 6724  crret 6769  crimt 6770  reim0t 6774  cjexpt 6817  absdivz 6859  recant 6905  bcnp11t 6965  bcpasc 6969  fsum1ps 7018  fsumsplit 7020  ser1ser0 7048  serzmulc 7058  climrecl 7110  climmullem3 7122  clim2serzt 7134  iserzmulc1 7136  clim2serz 7145  serzf0 7169  ser1f0 7170  isumclim3t 7200  isummulc1ALT 7213  fsum0diag3 7260  efaddlem14 7351  efsubt 7371  reeff1o 7426  sinnegt 7442  cosnegt 7443  infxpidmlem8 7559  subtop 7646  islp2 7747  cnpco 7769  iscncl 7770  cnconst 7780  dfms2 7799  metge0 7819  cnmet 7904  cncfmet 7905  bcthlem20 8018  isgrp 8041  isgrpi 8042  grpidinvlem2 8049  grpinvid2 8073  grpinvf 8079  grplactf1o 8098  ablmul 8131  ring2 8149  nvmtri2 8300  ipcj 8367  sspg 8387  ssps 8389  sspn 8395  nmlno0lem 8453  cnph 8478  ipasslem2 8491  siii 8513  minveclem23 8567  minveclem26 8570  minveclem36 8580  hlipcj 8613  abssinper 8712  cosh111lem2 8715  efifolem1 8722  efifolem6 8727  hiidge0t 8964  bcseq 8986  pjopt 9260  pjpot 9261  shunss 9337  h1de2 9476  fh1t 9561  fh2t 9562  pjot 9616  pjcj 9629  pjrn 9647  hmopret 9847  adjvalvalt 9861  hmopadjt 9863  hmoplint 9866  idhmop 9906  hmopbdopHIL 9912  nmlnop0ALT 9920  nmopunt 9939  cnvbravalt 10043  bracnlnvalt 10047  kbass3t 10051  pjhmop 10073  pjhmopidm 10110  hstoht 10159  sto2 10164  atom1d 10280  atcv0eq 10306  atcv1t 10307  moec 10461  fine2 10484  fine2OLD 10485  cdrci 10494  bsi 10495  hmphsyma 10528  hmeogrp 10538  set2elt 10545  setwoe 10546  oefil2 10567  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596  mslb1 10629  2wsms 10630  trran 10636  dcsda 10666  1ded 10671  rcmob 10682  1cat 10692  cmpassoh 10729  homgrf 10730  imonclem 10741  cmpmon 10743  icmpmon 10744  isfuna 10754  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain