Theorem eqcomd 2235

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

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

Syntax hints:   -> wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  eqtr2d  2263  eqtr3d  2264  eqtr4d  2265  eqtr2id  2275  eqtr2di  2279  sylan9req  2283  eqeltrrd  2307  eleqtrrd  2309  eleqtrrid  2319  eqeltrrdi  2321  eqnetrrd  2426  neeqtrrd  2430  rspcedeq2vd  2917  dedhb  2972  eqsstrrd  3261  sseqtrrd  3263  eqsstrrdi  3277  dfrab3ss  3482  uneqdifeqim  3577  ifbothdadc  3636  ifbothdc  3637  2if2dc  3642  disjsn2  3729  diftpsn3  3809  elpr2elpr  3854  dfopg  3855  unimax  3922  sndisj  4079  eqbrtrrd  4107  breqtrrd  4111  breqtrrid  4121  eqbrtrrdi  4123  class2seteq  4247  opth1  4322  euotd  4341  opelopabsb  4348  tfisi  4679  0nelxp  4747  opeliunxp  4774  euiotaex  5295  iota4  5298  iotam  5310  fun2ssres  5361  funimass1  5398  funssfv  5655  fnimapr  5696  fvun1  5702  fvco4  5708  elfvmptrab  5732  fmptco  5803  fncofn  5821  foima2  5881  foeqcnvco  5920  f1eqcocnv  5921  f1oiso2  5957  riotass2  5989  riotass  5990  f1ocnvfv3  5996  fvmpopr2d  6147  caovlem2d  6204  f1opw2  6218  offveq  6245  sbcopeq1a  6339  csbopeq1a  6340  eloprabi  6348  cnvf1olem  6376  f2ndf  6378  smoiso  6454  nnaword  6665  eqer  6720  uniqs  6748  mapsncnv  6850  ixpiinm  6879  mapsnf1o  6892  ssenen  7020  findcard2  7059  findcard2s  7060  unsnfidcex  7093  fisseneq  7107  phpeqd  7108  en1eqsn  7126  sbthlemi6  7140  updjud  7260  omp1eomlem  7272  nnnninf2  7305  nninfisollem0  7308  nninfisollemeq  7310  fodju0  7325  3nsssucpw1  7432  enq0sym  7630  enq0tr  7632  recexgt0sr  7971  caucvgsrlemoffcau  7996  axcaucvglemval  8095  le2tri3i  8266  cnegexlem2  8333  nnpcan  8380  addlsub  8527  negf1o  8539  subdi  8542  rereim  8744  cru  8760  divmulassap  8853  divmulasscomap  8854  divap1d  8959  subhalfhalf  9357  div4p1lem1div2  9376  difgtsumgt  9527  elz2  9529  zindd  9576  qapne  9846  divge1  9931  xrlttri3  10005  fseq1p1m1  10302  fzrevral  10313  nn0disj  10346  fzo0addel  10406  fzosplitsnm1  10427  fzosplitprm1  10452  flqlelt  10508  divfl0  10528  flqpmodeq  10561  zmodidfzo  10587  modqmuladd  10600  qnegmod  10603  addmodid  10606  modifeq2int  10620  modqeqmodmin  10628  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecuzrdgsuc  10648  frecfzen2  10661  iseqf1olemab  10736  iseqf1olemmo  10739  seqf1oglem1  10753  seqf1oglem2  10754  ser3sub  10757  expgt1  10811  leexp2r  10827  sqoddm1div8  10927  mulsubdivbinom2ap  10945  bcm1k  10994  bcn2m1  11003  hashinfuni  11011  hashennnuni  11013  hashennn  11014  hashunlem  11038  hashprg  11043  fihashssdif  11053  zfz1isolem1  11075  elovmpowrd  11126  ccatsymb  11150  ccatlid  11154  eqs1  11176  swrdfv2  11210  swrds1  11215  swrdlsw  11216  pfxfv  11231  swrdswrd  11252  swrdpfx  11254  pfxpfx  11255  pfxlswccat  11260  ccats1pfxeq  11261  wrdind  11269  wrd2ind  11270  pfxccatin12lem1  11275  pfxccatin12lem2  11278  swrdccat3blem  11286  swrdccat3b  11287  ccats1pfxeqbi  11289  reuccatpfxs1lem  11293  reuccatpfxs1  11294  shftlem  11342  shftfvalg  11344  shftfval  11347  replim  11385  cjexp  11419  resqrexlemcalc1  11540  resqrexlemcvg  11545  rersqrtthlem  11556  abssq  11607  recan  11635  negfi  11754  minclpr  11763  mingeb  11768  xrmaxiflemcom  11775  xrmineqinf  11795  xrminltinf  11798  xrminadd  11801  climmpt  11826  climrecl  11850  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  modfsummodlemstep  11983  isumsplit  12017  arisum  12024  geosergap  12032  geo2sum  12040  mertenslemi1  12061  mertenslem2  12062  clim2divap  12066  fproddccvg  12098  fprodssdc  12116  fprodabs  12142  fproddivapf  12157  fprodmodd  12167  efcj  12199  efsub  12207  eflegeo  12227  sinneg  12252  cosneg  12253  sin01bnd  12283  cos01bnd  12284  modm1div  12326  summodnegmod  12348  dvdseq  12374  addmodlteqALT  12385  mulmoddvds  12389  zob  12417  nn0ob  12434  divalgmod  12453  flodddiv4  12462  bitsinv1  12488  divgcdnnr  12512  gcdneg  12518  bezoutlemsup  12545  dvdssq  12567  lcmneg  12611  3lcm2e6woprm  12623  6lcm4e12  12624  divgcdcoprmex  12639  cncongr1  12640  cncongrcoprm  12643  oddpwdclemxy  12706  oddpwdclemodd  12709  divnumden  12733  zgcdsq  12738  phibnd  12754  hashgcdlem  12775  vfermltl  12789  powm2modprm  12790  reumodprminv  12791  pythagtriplem19  12820  pcprendvds2  12829  pczpre  12835  dvdsprmpweqle  12875  difsqpwdvds  12876  4sqlem4  12930  ennnfonelemex  13000  strndxid  13075  topnvalg  13299  prdssca  13323  intopsn  13415  ismgmid2  13428  mgmidsssn0  13432  gsumfzval  13439  gsumprval  13447  mndpfo  13486  mndfo  13487  mndinvmod  13493  prds0g  13497  mnd1id  13504  mhmf1o  13518  0mhm  13534  gsumwmhm  13546  grpidd2  13589  grpinvid2  13601  grpidssd  13624  grpnpcan  13640  grpsubsub4  13641  qusgrp2  13665  mulginvcom  13699  grpissubg  13746  quselbasg  13782  qus0  13787  ecqusaddd  13790  ghmid  13801  ghminv  13802  imasabl  13888  gsumfzmhm  13895  mgpress  13909  rnglz  13923  rngrz  13924  rngmneg1  13925  rngmneg2  13926  rngpropd  13933  srg1zr  13965  srgmulgass  13967  srgpcomp  13968  srgpcomppsc  13970  ringadd2  14005  ringo2times  14006  ringlz  14021  ringrz  14022  ringinvnzdiv  14028  ringnegl  14029  ringnegr  14030  imasring  14042  qusring2  14044  crngunit  14090  rhmopp  14155  lringuplu  14175  opprdomnbg  14253  lmod0vs  14300  lmodvsmmulgdi  14302  lmodfopne  14305  islss3  14358  lspsn  14395  lmodindp1  14407  rnglidlmmgm  14475  rnglidlmsgrp  14476  rnglidlrng  14477  isridl  14483  zringinvg  14583  zndvds  14628  znf1o  14630  psrgrp  14664  toponcom  14716  tgtopon  14755  restopnb  14870  cnptoprest  14928  blfvalps  15074  bdmopn  15193  cnmet  15219  mpomulcn  15255  limcdifap  15351  dvidsslem  15382  dviaddf  15394  dvexp  15400  dvply2g  15455  coseq0negpitopi  15525  abssinper  15535  rplogbzexp  15643  dvdsppwf1o  15678  mpodvdsmulf1o  15679  fsumdvdsmul  15680  sgmmul  15685  perfect  15690  lgsvalmod  15713  lgsneg  15718  gausslemma2dlem1a  15752  gausslemma2dlem6  15761  gausslemma2dlem7  15762  gausslemma2d  15763  lgsquadlem2  15772  2lgslem1a1  15780  2lgslem1a  15782  2lgslem3c  15789  2lgslem3d  15790  2lgslem3d1  15794  2lgs  15798  2lgsoddprm  15807  uhgrun  15901  upgrun  15939  umgrun  15941  ushgredgedg  16039  wlklenvm1  16082  wlklenvm1g  16083  wlkl1loop  16099  upgriswlkdc  16101  uspgr2wlkeq  16106  uspgr2wlkeq2  16107  uspgr2wlkeqi  16108  wlkres  16118  subctctexmid  16425  cvgcmp2nlemabs  16460  trilpolemlt1  16469