Theorem eqcomd 2244

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2d  2272  eqtr3d  2273  eqtr4d  2274  eqtr2id  2284  eqtr2di  2288  sylan9req  2292  eqeltrrd  2316  eleqtrrd  2318  eleqtrrid  2328  eqeltrrdi  2330  eqabcdv  2370  eqnetrrd  2446  neeqtrrd  2450  rspcedeq2vd  2940  dedhb  2995  eqsstrrd  3285  sseqtrrd  3287  eqsstrrdi  3301  dfrab3ss  3511  uneqdifeqim  3613  ifbothdadc  3674  ifbothdc  3675  2if2dc  3680  ifeqeqxdc  3687  disjsn2  3772  diftpsn3  3856  elpr2elpr  3901  dfopg  3902  unimax  3969  sndisj  4126  eqbrtrrd  4154  breqtrrd  4158  breqtrrid  4168  eqbrtrrdi  4170  class2seteq  4300  opth1  4376  euotd  4395  opelopabsb  4402  tfisi  4734  0nelxp  4802  opeliunxp  4830  euiotaex  5354  iota4  5357  iotam  5369  fun2ssres  5421  funimass1  5458  funssfv  5721  fnimapr  5763  fvun1  5769  fvco4  5777  elfvmptrab  5802  fmptco  5874  fncofn  5893  foima2  5957  foeqcnvco  5996  f1eqcocnv  5997  f1oiso2  6033  riotass2  6067  riotass  6068  f1ocnvfv3  6074  fvmpopr2d  6225  caovlem2d  6282  f1opw2  6296  offveq  6323  sbcopeq1a  6421  csbopeq1a  6422  eloprabi  6432  cnvf1olem  6460  f2ndf  6462  suppval1  6479  suppsnopdc  6490  smoiso  6573  nnaword  6784  eqer  6839  uniqs  6867  mapsncnv  6977  ixpiinm  7006  mapsnf1o  7019  mapunen  7151  ssenen  7152  findcard2  7193  findcard2s  7194  unsnfidcex  7227  fisseneq  7242  phpeqd  7243  en1eqsn  7265  sbthlemi6  7279  updjud  7423  omp1eomlem  7435  nnnninf2  7468  nninfisollem0  7471  nninfisollemeq  7473  fodju0  7488  3nsssucpw1  7596  enq0sym  7800  enq0tr  7802  recexgt0sr  8141  caucvgsrlemoffcau  8166  axcaucvglemval  8265  le2tri3i  8436  cnegexlem2  8504  nnpcan  8551  addlsub  8698  negf1o  8711  subdi  8714  rereim  8917  cru  8933  divmulassap  9028  divmulasscomap  9029  divap1d  9134  subhalfhalf  9545  div4p1lem1div2  9564  difgtsumgt  9719  elz2  9721  zindd  9769  qapne  10049  divge1  10135  xrlttri3  10210  fseq1p1m1  10512  fzrevral  10523  nn0disj  10556  fzo0addel  10617  fzosplitsnm1  10638  fzosplitprm1  10664  flqlelt  10723  flaplelt  10724  divfl0  10746  flqpmodeq  10779  zmodidfzo  10805  modqmuladd  10818  qnegmod  10821  addmodid  10824  modifeq2int  10838  modqeqmodmin  10846  modfzo0difsn  10847  modsumfzodifsn  10848  addmodlteq  10850  frecuzrdgsuc  10866  frecfzen2  10879  iseqf1olemab  10954  iseqf1olemmo  10957  seqf1oglem1  10971  seqf1oglem2  10972  ser3sub  10975  expgt1  11029  leexp2r  11045  sqoddm1div8  11146  mulsubdivbinom2ap  11165  bcm1k  11214  bcn2m1  11224  hashinfuni  11232  hashennnuni  11234  hashennn  11235  hashunlem  11260  hashprg  11265  fihashssdif  11275  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  zfz1isolem1  11308  elovmpowrd  11362  ccatsymb  11386  ccatlid  11390  eqs1  11412  ccatw2s1p1g  11429  swrdfv2  11451  swrds1  11456  swrdlsw  11457  pfxfv  11472  swrdswrd  11493  swrdpfx  11495  pfxpfx  11496  pfxlswccat  11501  ccats1pfxeq  11502  wrdind  11510  wrd2ind  11511  pfxccatin12lem1  11516  pfxccatin12lem2  11519  swrdccat3blem  11527  swrdccat3b  11528  ccats1pfxeqbi  11530  reuccatpfxs1lem  11534  reuccatpfxs1  11535  s3s4d  11591  s2s5d  11592  s5s2d  11593  shftlem  11597  shftfvalg  11599  shftfval  11602  replim  11640  cjexp  11674  sq01  11676  resqrexlemcalc1  11796  resqrexlemcvg  11801  rersqrtthlem  11812  abssq  11864  recan  11892  negfi  12011  minclpr  12021  mingeb  12027  xrmaxiflemcom  12034  xrmineqinf  12054  xrminltinf  12057  xrminadd  12060  climmpt  12085  climrecl  12109  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  modfsummodlemstep  12243  isumsplit  12277  arisum  12284  geosergap  12292  geo2sum  12300  mertenslemi1  12321  mertenslem2  12322  clim2divap  12326  fproddccvg  12358  fprodssdc  12376  fprodabs  12402  fproddivapf  12417  fprodmodd  12427  efcj  12459  efsub  12467  eflegeo  12487  sinneg  12512  cosneg  12513  sin01bnd  12543  cos01bnd  12544  modm1div  12586  summodnegmod  12608  dvdseq  12634  addmodlteqALT  12645  mulmoddvds  12649  zob  12677  nn0ob  12694  divalgmod  12713  flodddiv4  12722  bitsinv1  12748  divgcdnnr  12772  gcdneg  12778  bezoutlemsup  12805  dvdssq  12827  lcmneg  12871  3lcm2e6woprm  12883  6lcm4e12  12884  divgcdcoprmex  12899  cncongr1  12900  cncongrcoprm  12903  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  divnumden  12995  zgcdsq  13000  phibnd  13018  hashgcdlem  13039  vfermltl  13053  powm2modprm  13054  reumodprminv  13055  pythagtriplem19  13084  pcprendvds2  13093  pczpre  13099  dvdsprmpweqle  13139  difsqpwdvds  13140  4sqlem4  13194  prmlem0  13243  ballotfilemfp1  13283  ballotfilemsf1o  13309  ballotfilemrinv0  13328  ennnfonelemex  13357  strndxid  13432  topnvalg  13658  intopsn  13740  ismgmid2  13753  mgmidsssn0  13757  gzsumfzval  13764  mndpfo  13804  mndfo  13805  mndinvmod  13811  mnd1id  13816  mhmf1o  13830  0mhm  13846  gzsumwmhm  13856  grpidd2  13899  grpinvid2  13911  grpidssd  13934  grpnpcan  13950  grpsubsub4  13951  qusgrp2  13969  mulginvcom  14003  grpissubg  14050  quselbasg  14086  qus0  14091  ecqusaddd  14094  ghmid  14105  ghminv  14106  cntrval  14145  imasabl  14224  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  gsumsncmn  14240  prdssca  14259  prds0g  14279  mgpress  14314  rnglz  14328  rngrz  14329  rngmneg1  14330  rngmneg2  14331  rngpropd  14338  rng1zrlem  14342  srgmulgass  14377  srgpcomp  14378  srgpcomppsc  14380  ringadd2  14416  ringo2times  14417  ringlz  14432  ringrz  14433  ringinvnzdiv  14439  ringnegl  14440  ringnegr  14441  imasring  14453  qusring2  14455  crngunit  14502  rhmopp  14567  lringuplu  14587  opprdomnbg  14667  lmod0vs  14742  lmodvsmmulgdi  14744  lmodfopne  14747  islss3  14800  lspsn  14837  lmodindp1  14849  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  isridl  14925  zringinvg  15023  zndvds  15068  znf1o  15070  assa2ass  15093  assa2ass2  15094  asclinvg  15116  assamulgscmlem1  15125  assamulgscmlem2  15126  psrgrp  15167  toponcom  15219  tgtopon  15258  restopnb  15373  cnptoprest  15431  blfvalps  15577  bdmopn  15696  cnmet  15722  mpomulcn  15758  limcdifap  15854  dvidsslem  15885  dviaddf  15897  dvexp  15903  dvply2g  15958  coseq0negpitopi  16029  abssinper  16039  rplogbzexp  16151  pellexlem2  16191  dvdsppwf1o  16244  mpodvdsmulf1o  16245  fsumdvdsmul  16246  sgmmul  16251  perfect  16262  bcmono  16265  prmefexple  16269  bposlem1  16272  bposlem9  16280  lgsvalmod  16304  lgsneg  16309  gausslemma2dlem1a  16343  gausslemma2dlem6  16352  gausslemma2dlem7  16353  gausslemma2d  16354  lgsquadlem2  16363  2lgslem1a1  16371  2lgslem1a  16373  2lgslem3c  16380  2lgslem3d  16381  2lgslem3d1  16385  2lgs  16389  2lgsoddprm  16398  uhgrun  16493  upgrun  16533  umgrun  16535  ushgredgedg  16633  issubgr2  16665  uhgrissubgr  16668  subgruhgredgdm  16677  subumgredg2en  16678  subupgr  16680  p1evtxdeqfilem  16718  wlklenvm1  16748  wlklenvm1g  16749  wlkl1loop  16765  upgriswlkdc  16767  uspgr2wlkeq  16772  uspgr2wlkeq2  16773  uspgr2wlkeqi  16774  wlkres  16786  loopclwwlkn1b  16826  clwwlkn1loopb  16827  clwwlkext2edg  16829  clwwlknonccat  16840  s2elclwwlknon2  16843  clwwlknonex2lem2  16845  clwwlknun  16848  eupth2lem3fi  16883  eupth2lembfi  16884  subctctexmid  17196  cvgcmp2nlemabs  17247  trilpolemlt1  17257