Theorem eqcoms 2748

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
eqcoms.1	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
eqcoms	⊢ (𝐵 = 𝐴 → 𝜑)

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2747	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 218	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  gencbvex  3490  sbceq2a  3742  eqimss2  3981  uneqdifeq  4427  tppreq3  4698  ifpprsnss  4703  tpprceq3  4744  preqsnd  4797  prproe  4843  copsex2t  5440  snopeqop  5454  opthhausdorff0  5466  optocl  5719  relopabi  5772  cnvimassrndm  6110  cnveqb  6154  cnveq0  6155  unixpid  6242  reuop  6251  f0rn0  6719  fimadmfo  6755  f1ssf1  6806  tz6.12i  6860  fveqdmss  7026  fvcofneq  7041  funopsnOLD  7098  f1ocnvfv  7229  f1ocnvfvb  7230  cbvfo  7240  riotaeqimp  7346  ov6g  7527  tfindsg  7808  findsg  7844  mptcnfimad  7935  suppimacnv  8121  ectocld  8726  ecoptocl  8751  undifixp  8879  f1dmvrnfibi  9248  f1vrnfibi  9249  updjud  9856  card1  9890  prdom2  9926  sornom  10197  indpi  10828  ltlen  11245  eqlei  11254  squeeze0  12057  nn0ind-raph  12627  fzoopth  13715  injresinjlem  13743  fvf1tp  13746  modmuladd  13873  modmuladdnn0  13875  hashf1rn  14312  hashrabsn1  14334  hash1snb  14379  hashgt12el  14382  hashgt12el2  14383  hashfzp1  14391  hash2prde  14430  hash2pwpr  14436  fi1uzind  14467  brfi1indALT  14470  lswlgt0cl  14529  wrd2ind  14683  pfxccatin12lem2  14691  pfxccatin12lem3  14692  cshweqrep  14781  scshwfzeqfzo  14786  cshimadifsn  14789  cshimadifsn0  14790  2swrd2eqwrdeq  14913  wwlktovfo  14918  rennim  15199  absmod0  15263  modfsummods  15754  mod2eq1n2dvds  16314  m1expe  16341  m1expo  16342  m1exp1  16343  nn0o1gt2  16348  flodddiv4  16382  cncongr1  16634  ge2nprmge4  16669  m1dvdsndvds  16767  cshwrepswhash1  17071  initoeu2lem1  17979  istos  18380  mgmsscl  18611  mndinvmod  18730  smndex1n0mnd  18881  symgfvne  19354  symgfix2  19389  symgextf1  19394  symgfixelsi  19408  psgnsn  19493  odbezout  19531  cntzcmnss  19814  frgpnabllem1  19846  ringinvnzdiv  20280  rngcinv  20616  psgndiflemB  21582  uvcendim  21829  selvvvval  22125  mamufacex  22386  smatvscl  22514  mavmulsolcl  22541  mdetunilem8  22609  pm2mpfo  22804  chpscmat  22832  chmaidscmat  22838  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  txcn  23616  qtopeu  23706  reeff1o  26437  relogbcxpb  26776  logbgcd1irr  26783  fsumdvdsmul  27183  zabsle1  27284  2lgslem1c  27381  2lgsoddprmlem3  27402  2sq2  27421  2sqreultlem  27435  2sqreunnltlem  27438  2sqreulem3  27441  pntrlog2bndlem5  27569  ltlesnd  27764  upgrpredgv  29233  usgredg2vlem2  29320  ushgredgedg  29323  ushgredgedgloop  29325  uhgrspan1  29397  nb3grprlem1  29474  uvtxnbgrb  29495  cusgrsize2inds  29547  1egrvtxdg0  29605  uspgrloopvtxel  29610  finsumvtxdg2size  29644  rusgrpropnb  29677  ifpsnprss  29716  upgrwlkvtxedg  29738  uspgr2wlkeq  29739  wlkp1lem5  29769  wlkp1  29773  usgr2pth  29857  uspgrn2crct  29901  iswwlksnon  29946  wlkiswwlks1  29960  wlkiswwlks2lem3  29964  wwlksnextbi  29987  wwlksnredwwlkn0  29989  wwlksnextwrd  29990  wwlksnextsurj  29993  wwlksnextprop  30005  wspn0  30017  umgr2adedgwlkonALT  30040  umgr2adedgspth  30041  umgr2wlkon  30043  elwwlks2ons3  30048  elwwlks2on  30054  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlkf1lem3  30101  clwwlkfo  30145  eleclclwwlknlem2  30156  erclwwlkntr  30166  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  0wlkonlem1  30213  upgr1wlkdlem1  30240  1pthon2v  30248  upgr3v3e3cycl  30275  uhgr3cyclexlem  30276  upgr4cycl4dv4e  30280  eupth2lem3lem3  30325  eupth2lem3lem4  30326  1to2vfriswmgr  30374  frgrncvvdeqlem6  30399  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  frgrwopreglem2  30408  2clwwlk2clwwlk  30445  extwwlkfab  30447  numclwwlk1lem2f1  30452  numclwwlkovh  30468  numclwwlk2lem1  30471  numclwlk2lem2f  30472  cdj1i  32529  brabgaf  32705  br8d  32707  sgn3da  32933  onvf1odlem1  35338  spthcycl  35364  goalrlem  35631  goalr  35632  fmlasucdisj  35634  satffunlem  35636  satffunlem1lem1  35637  satffunlem1lem2  35638  satffunlem2lem1  35639  satffunlem2lem2  35641  mthmb  35816  br8  35991  br4  35993  bj-snsetex  37323  bj-snglc  37329  copsex2d  37506  wl-dfcleq  37883  poimirlem20  38014  poimirlem26  38020  poimirlem27  38021  mblfinlem3  38033  mblfinlem4  38034  itg2addnclem  38045  indexdom  38108  ismgmOLD  38224  rngodm1dm2  38306  rngomndo  38309  rngoueqz  38314  zerdivemp1x  38321  opcon3b  39695  ps-1  39976  3atlem5  39986  4atex  40575  prjspvs  43067  iscard4  43984  pr2cv  43999  pm13.192  44861  iotavalsb  44884  relpfrlem  45404  fourierdlem32  46589  fourierdlem49  46605  fourierdlem64  46620  elprneb  47499  fveqvfvv  47510  funressnfv  47513  f1cof1b  47547  nvelim  47593  afvpcfv0  47616  afv0nbfvbi  47621  fnbrafvb  47624  tz6.12-afv  47643  afvco2  47646  ndmaovg  47654  afv2orxorb  47698  tz6.12-afv2  47710  tz6.12i-afv2  47713  f1oresf1o2  47761  nnmul2  47800  elsetpreimafvbi  47873  imasetpreimafvbijlemfo  47887  iccpartiltu  47904  fargshiftfv  47921  fargshiftf  47922  lswn0  47926  prsprel  47969  reupr  48004  2exopprim  48007  fmtnorec2lem  48027  2pwp1prm  48074  lighneallem2  48091  lighneallem3  48092  proththd  48099  ppivalnnprm  48110  ppivalnnnprmge6  48111  nn0o1gt2ALTV  48192  evenltle  48215  sbgoldbwt  48275  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  clnbgrval  48320  dfvopnbgr2  48351  uhgrimedgi  48388  gricushgr  48415  clnbgrgrim  48432  grimedg  48433  cycl3grtri  48445  isubgr3stgrlem4  48467  uspgrlimlem1  48486  grlimgrtri  48501  gpgedg2ov  48564  gpgedg2iv  48565  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem4  48617  uspgropssxp  48642  lmod0rng  48727  lidldomn1  48729  zlidlring  48732  rngcinvALTV  48774  ztprmneprm  48845  lincext3  48954  zlmodzxznm  48995  suppdm  49008  elfzolborelfzop1  49017  nn0sumshdiglemB  49118  itcovalsucov  49166  lines  49229  rrx2vlinest  49239  line2xlem  49251  itschlc0yqe  49258  itsclquadeu  49275