Theorem eqcoms 2739

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 2738	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 217	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  gencbvex  3495  sbceq2a  3748  eqimss2  3989  uneqdifeq  4442  tppreq3  4711  ifpprsnss  4716  tpprceq3  4755  preqsnd  4810  prproe  4856  copsex2t  5435  snopeqop  5449  opthhausdorff0  5461  optocl  5713  relopabi  5767  cnvimassrndm  6105  cnveqb  6149  cnveq0  6150  unixpid  6237  reuop  6246  f0rn0  6714  fimadmfo  6750  f1ssf1  6801  tz6.12i  6854  fveqdmss  7017  fvcofneq  7032  funopsn  7087  f1ocnvfv  7218  f1ocnvfvb  7219  cbvfo  7229  riotaeqimp  7335  ov6g  7516  tfindsg  7797  findsg  7833  mptcnfimad  7924  suppimacnv  8110  ectocld  8712  ecoptocl  8737  undifixp  8864  f1dmvrnfibi  9231  f1vrnfibi  9232  updjud  9833  card1  9867  prdom2  9903  sornom  10174  indpi  10804  ltlen  11220  eqlei  11229  squeeze0  12031  nn0ind-raph  12579  fzoopth  13668  injresinjlem  13696  fvf1tp  13699  modmuladd  13826  modmuladdnn0  13828  hashf1rn  14265  hashrabsn1  14287  hash1snb  14332  hashgt12el  14335  hashgt12el2  14336  hashfzp1  14344  hash2prde  14383  hash2pwpr  14389  fi1uzind  14420  brfi1indALT  14423  lswlgt0cl  14482  wrd2ind  14636  pfxccatin12lem2  14644  pfxccatin12lem3  14645  cshweqrep  14734  scshwfzeqfzo  14739  cshimadifsn  14742  cshimadifsn0  14743  2swrd2eqwrdeq  14866  wwlktovfo  14871  rennim  15152  absmod0  15216  modfsummods  15706  mod2eq1n2dvds  16264  m1expe  16291  m1expo  16292  m1exp1  16293  nn0o1gt2  16298  flodddiv4  16332  cncongr1  16584  ge2nprmge4  16618  m1dvdsndvds  16716  cshwrepswhash1  17020  initoeu2lem1  17927  istos  18328  mgmsscl  18559  mndinvmod  18678  smndex1n0mnd  18826  symgfvne  19299  symgfix2  19334  symgextf1  19339  symgfixelsi  19353  psgnsn  19438  odbezout  19476  cntzcmnss  19759  frgpnabllem1  19791  ringinvnzdiv  20225  rngcinv  20558  psgndiflemB  21543  uvcendim  21790  mamufacex  22317  smatvscl  22445  mavmulsolcl  22472  mdetunilem8  22540  pm2mpfo  22735  chpscmat  22763  chmaidscmat  22769  chfacfscmulgsum  22781  chfacfpmmulgsum  22785  txcn  23547  qtopeu  23637  reeff1o  26390  relogbcxpb  26730  logbgcd1irr  26737  fsumdvdsmul  27138  zabsle1  27240  2lgslem1c  27337  2lgsoddprmlem3  27358  2sq2  27377  2sqreultlem  27391  2sqreunnltlem  27394  2sqreulem3  27397  pntrlog2bndlem5  27525  sltlend  27716  upgrpredgv  29124  usgredg2vlem2  29211  ushgredgedg  29214  ushgredgedgloop  29216  uhgrspan1  29288  nb3grprlem1  29365  uvtxnbgrb  29386  cusgrsize2inds  29439  1egrvtxdg0  29497  uspgrloopvtxel  29502  finsumvtxdg2size  29536  rusgrpropnb  29569  ifpsnprss  29608  upgrwlkvtxedg  29630  uspgr2wlkeq  29631  wlkp1lem5  29661  wlkp1  29665  usgr2pth  29749  uspgrn2crct  29793  iswwlksnon  29838  wlkiswwlks1  29852  wlkiswwlks2lem3  29856  wwlksnextbi  29879  wwlksnredwwlkn0  29881  wwlksnextwrd  29882  wwlksnextsurj  29885  wwlksnextprop  29897  wspn0  29909  umgr2adedgwlkonALT  29932  umgr2adedgspth  29933  umgr2wlkon  29935  elwwlks2ons3  29940  elwwlks2on  29946  clwlkclwwlklem2a4  29984  clwlkclwwlklem2a  29985  clwlkclwwlkf1lem3  29993  clwwlkfo  30037  eleclclwwlknlem2  30048  erclwwlkntr  30058  hashecclwwlkn1  30064  umgrhashecclwwlk  30065  0wlkonlem1  30105  upgr1wlkdlem1  30132  1pthon2v  30140  upgr3v3e3cycl  30167  uhgr3cyclexlem  30168  upgr4cycl4dv4e  30172  eupth2lem3lem3  30217  eupth2lem3lem4  30218  1to2vfriswmgr  30266  frgrncvvdeqlem6  30291  frgrncvvdeqlem8  30293  frgrncvvdeqlem9  30294  frgrwopreglem2  30300  2clwwlk2clwwlk  30337  extwwlkfab  30339  numclwwlk1lem2f1  30344  numclwwlkovh  30360  numclwwlk2lem1  30363  numclwlk2lem2f  30364  cdj1i  32420  brabgaf  32596  br8d  32598  sgn3da  32824  onvf1odlem1  35154  spthcycl  35180  goalrlem  35447  goalr  35448  fmlasucdisj  35450  satffunlem  35452  satffunlem1lem1  35453  satffunlem1lem2  35454  satffunlem2lem1  35455  satffunlem2lem2  35457  mthmb  35632  br8  35807  br4  35809  bj-snsetex  37014  bj-snglc  37020  copsex2d  37190  poimirlem20  37686  poimirlem26  37692  poimirlem27  37693  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem  37717  indexdom  37780  ismgmOLD  37896  rngodm1dm2  37978  rngomndo  37981  rngoueqz  37986  zerdivemp1x  37993  opcon3b  39301  ps-1  39582  3atlem5  39592  4atex  40181  selvvvval  42684  prjspvs  42709  iscard4  43631  pr2cv  43646  pm13.192  44508  iotavalsb  44531  relpfrlem  45051  fourierdlem32  46242  fourierdlem49  46258  fourierdlem64  46273  elprneb  47134  fveqvfvv  47145  funressnfv  47148  f1cof1b  47182  nvelim  47228  afvpcfv0  47251  afv0nbfvbi  47256  fnbrafvb  47259  tz6.12-afv  47278  afvco2  47281  ndmaovg  47289  afv2orxorb  47333  tz6.12-afv2  47345  tz6.12i-afv2  47348  f1oresf1o2  47396  elsetpreimafvbi  47496  imasetpreimafvbijlemfo  47510  iccpartiltu  47527  fargshiftfv  47544  fargshiftf  47545  lswn0  47549  prsprel  47592  reupr  47627  2exopprim  47630  fmtnorec2lem  47647  2pwp1prm  47694  lighneallem2  47711  lighneallem3  47712  proththd  47719  nn0o1gt2ALTV  47799  evenltle  47822  sbgoldbwt  47882  nnsum4primeseven  47905  nnsum4primesevenALTV  47906  clnbgrval  47927  dfvopnbgr2  47958  uhgrimedgi  47995  gricushgr  48022  clnbgrgrim  48039  grimedg  48040  cycl3grtri  48052  isubgr3stgrlem4  48074  uspgrlimlem1  48093  grlimgrtri  48108  gpgedg2ov  48171  gpgedg2iv  48172  pgnbgreunbgrlem1  48218  pgnbgreunbgrlem2lem3  48221  pgnbgreunbgrlem2  48222  pgnbgreunbgrlem4  48224  uspgropssxp  48249  lmod0rng  48334  lidldomn1  48336  zlidlring  48339  rngcinvALTV  48381  ztprmneprm  48452  lincext3  48562  zlmodzxznm  48603  suppdm  48616  elfzolborelfzop1  48625  nn0sumshdiglemB  48726  itcovalsucov  48774  lines  48837  rrx2vlinest  48847  line2xlem  48859  itschlc0yqe  48866  itsclquadeu  48883