Theorem eqcoms 2744

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  gencbvex  3487  sbceq2a  3740  eqimss2  3981  uneqdifeq  4432  tppreq3  4703  ifpprsnss  4708  tpprceq3  4749  preqsnd  4802  prproe  4848  copsex2t  5446  snopeqop  5460  opthhausdorff0  5472  optocl  5725  relopabi  5778  cnvimassrndm  6116  cnveqb  6160  cnveq0  6161  unixpid  6248  reuop  6257  f0rn0  6725  fimadmfo  6761  f1ssf1  6812  tz6.12i  6866  fveqdmss  7030  fvcofneq  7045  funopsnOLD  7102  f1ocnvfv  7233  f1ocnvfvb  7234  cbvfo  7244  riotaeqimp  7350  ov6g  7531  tfindsg  7812  findsg  7848  mptcnfimad  7939  suppimacnv  8124  ectocld  8729  ecoptocl  8754  undifixp  8882  f1dmvrnfibi  9251  f1vrnfibi  9252  updjud  9858  card1  9892  prdom2  9928  sornom  10199  indpi  10830  ltlen  11247  eqlei  11256  squeeze0  12059  nn0ind-raph  12629  fzoopth  13717  injresinjlem  13745  fvf1tp  13748  modmuladd  13875  modmuladdnn0  13877  hashf1rn  14314  hashrabsn1  14336  hash1snb  14381  hashgt12el  14384  hashgt12el2  14385  hashfzp1  14393  hash2prde  14432  hash2pwpr  14438  fi1uzind  14469  brfi1indALT  14472  lswlgt0cl  14531  wrd2ind  14685  pfxccatin12lem2  14693  pfxccatin12lem3  14694  cshweqrep  14783  scshwfzeqfzo  14788  cshimadifsn  14791  cshimadifsn0  14792  2swrd2eqwrdeq  14915  wwlktovfo  14920  rennim  15201  absmod0  15265  modfsummods  15756  mod2eq1n2dvds  16316  m1expe  16343  m1expo  16344  m1exp1  16345  nn0o1gt2  16350  flodddiv4  16384  cncongr1  16636  ge2nprmge4  16671  m1dvdsndvds  16769  cshwrepswhash1  17073  initoeu2lem1  17981  istos  18382  mgmsscl  18613  mndinvmod  18732  smndex1n0mnd  18883  symgfvne  19356  symgfix2  19391  symgextf1  19396  symgfixelsi  19410  psgnsn  19495  odbezout  19533  cntzcmnss  19816  frgpnabllem1  19848  ringinvnzdiv  20282  rngcinv  20614  psgndiflemB  21580  uvcendim  21827  mamufacex  22361  smatvscl  22489  mavmulsolcl  22516  mdetunilem8  22584  pm2mpfo  22779  chpscmat  22807  chmaidscmat  22813  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  txcn  23591  qtopeu  23681  reeff1o  26412  relogbcxpb  26751  logbgcd1irr  26758  fsumdvdsmul  27158  zabsle1  27259  2lgslem1c  27356  2lgsoddprmlem3  27377  2sq2  27396  2sqreultlem  27410  2sqreunnltlem  27413  2sqreulem3  27416  pntrlog2bndlem5  27544  ltlesnd  27739  upgrpredgv  29208  usgredg2vlem2  29295  ushgredgedg  29298  ushgredgedgloop  29300  uhgrspan1  29372  nb3grprlem1  29449  uvtxnbgrb  29470  cusgrsize2inds  29522  1egrvtxdg0  29580  uspgrloopvtxel  29585  finsumvtxdg2size  29619  rusgrpropnb  29652  ifpsnprss  29691  upgrwlkvtxedg  29713  uspgr2wlkeq  29714  wlkp1lem5  29744  wlkp1  29748  usgr2pth  29832  uspgrn2crct  29876  iswwlksnon  29921  wlkiswwlks1  29935  wlkiswwlks2lem3  29939  wwlksnextbi  29962  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  wwlksnextsurj  29968  wwlksnextprop  29980  wspn0  29992  umgr2adedgwlkonALT  30015  umgr2adedgspth  30016  umgr2wlkon  30018  elwwlks2ons3  30023  elwwlks2on  30029  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlkf1lem3  30076  clwwlkfo  30120  eleclclwwlknlem2  30131  erclwwlkntr  30141  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  0wlkonlem1  30188  upgr1wlkdlem1  30215  1pthon2v  30223  upgr3v3e3cycl  30250  uhgr3cyclexlem  30251  upgr4cycl4dv4e  30255  eupth2lem3lem3  30300  eupth2lem3lem4  30301  1to2vfriswmgr  30349  frgrncvvdeqlem6  30374  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrwopreglem2  30383  2clwwlk2clwwlk  30420  extwwlkfab  30422  numclwwlk1lem2f1  30427  numclwwlkovh  30443  numclwwlk2lem1  30446  numclwlk2lem2f  30447  cdj1i  32504  brabgaf  32679  br8d  32681  sgn3da  32907  onvf1odlem1  35285  spthcycl  35311  goalrlem  35578  goalr  35579  fmlasucdisj  35581  satffunlem  35583  satffunlem1lem1  35584  satffunlem1lem2  35585  satffunlem2lem1  35586  satffunlem2lem2  35588  mthmb  35763  br8  35938  br4  35940  bj-snsetex  37270  bj-snglc  37276  copsex2d  37453  wl-dfcleq  37830  poimirlem20  37961  poimirlem26  37967  poimirlem27  37968  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  indexdom  38055  ismgmOLD  38171  rngodm1dm2  38253  rngomndo  38256  rngoueqz  38261  zerdivemp1x  38268  opcon3b  39642  ps-1  39923  3atlem5  39933  4atex  40522  selvvvval  43018  prjspvs  43043  iscard4  43960  pr2cv  43975  pm13.192  44837  iotavalsb  44860  relpfrlem  45380  fourierdlem32  46567  fourierdlem49  46583  fourierdlem64  46598  elprneb  47477  fveqvfvv  47488  funressnfv  47491  f1cof1b  47525  nvelim  47571  afvpcfv0  47594  afv0nbfvbi  47599  fnbrafvb  47602  tz6.12-afv  47621  afvco2  47624  ndmaovg  47632  afv2orxorb  47676  tz6.12-afv2  47688  tz6.12i-afv2  47691  f1oresf1o2  47739  nnmul2  47778  elsetpreimafvbi  47851  imasetpreimafvbijlemfo  47865  iccpartiltu  47882  fargshiftfv  47899  fargshiftf  47900  lswn0  47904  prsprel  47947  reupr  47982  2exopprim  47985  fmtnorec2lem  48005  2pwp1prm  48052  lighneallem2  48069  lighneallem3  48070  proththd  48077  ppivalnnprm  48088  ppivalnnnprmge6  48089  nn0o1gt2ALTV  48170  evenltle  48193  sbgoldbwt  48253  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  clnbgrval  48298  dfvopnbgr2  48329  uhgrimedgi  48366  gricushgr  48393  clnbgrgrim  48410  grimedg  48411  cycl3grtri  48423  isubgr3stgrlem4  48445  uspgrlimlem1  48464  grlimgrtri  48479  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  uspgropssxp  48620  lmod0rng  48705  lidldomn1  48707  zlidlring  48710  rngcinvALTV  48752  ztprmneprm  48823  lincext3  48932  zlmodzxznm  48973  suppdm  48986  elfzolborelfzop1  48995  nn0sumshdiglemB  49096  itcovalsucov  49144  lines  49207  rrx2vlinest  49217  line2xlem  49229  itschlc0yqe  49236  itsclquadeu  49253