Theorem eqcoms 2738

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  gencbvex  3510  sbceq2a  3768  eqimss2  4009  uneqdifeq  4459  tppreq3  4726  ifpprsnss  4731  tpprceq3  4771  preqsnd  4826  prproe  4872  copsex2t  5455  snopeqop  5469  opthhausdorff0  5481  relopabi  5788  cnvimassrndm  6128  cnveqb  6172  cnveq0  6173  unixpid  6260  reuop  6269  f0rn0  6748  fimadmfo  6784  f1ssf1  6835  tz6.12i  6889  fveqdmss  7053  fvcofneq  7068  funopsn  7123  f1ocnvfv  7256  f1ocnvfvb  7257  cbvfo  7267  riotaeqimp  7373  ov6g  7556  tfindsg  7840  findsg  7876  mptcnfimad  7968  suppimacnv  8156  ectocld  8758  ecoptocl  8783  undifixp  8910  f1dmvrnfibi  9299  f1vrnfibi  9300  updjud  9894  card1  9928  pr2neOLD  9965  prdom2  9966  sornom  10237  indpi  10867  ltlen  11282  eqlei  11291  squeeze0  12093  nn0ind-raph  12641  fzoopth  13730  injresinjlem  13755  fvf1tp  13758  modmuladd  13885  modmuladdnn0  13887  hashf1rn  14324  hashrabsn1  14346  hash1snb  14391  hashgt12el  14394  hashgt12el2  14395  hashfzp1  14403  hash2prde  14442  hash2pwpr  14448  fi1uzind  14479  brfi1indALT  14482  lswlgt0cl  14541  wrd2ind  14695  pfxccatin12lem2  14703  pfxccatin12lem3  14704  cshweqrep  14793  cshwsexaOLD  14797  scshwfzeqfzo  14799  cshimadifsn  14802  cshimadifsn0  14803  2swrd2eqwrdeq  14926  wwlktovfo  14931  rennim  15212  absmod0  15276  modfsummods  15766  mod2eq1n2dvds  16324  m1expe  16351  m1expo  16352  m1exp1  16353  nn0o1gt2  16358  flodddiv4  16392  cncongr1  16644  ge2nprmge4  16678  m1dvdsndvds  16776  cshwrepswhash1  17080  initoeu2lem1  17983  istos  18384  mgmsscl  18579  mndinvmod  18698  smndex1n0mnd  18846  symgfvne  19318  symgfix2  19353  symgextf1  19358  symgfixelsi  19372  psgnsn  19457  odbezout  19495  cntzcmnss  19778  frgpnabllem1  19810  ringinvnzdiv  20217  rngcinv  20553  psgndiflemB  21516  uvcendim  21763  mamufacex  22290  smatvscl  22418  mavmulsolcl  22445  mdetunilem8  22513  pm2mpfo  22708  chpscmat  22736  chmaidscmat  22742  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  txcn  23520  qtopeu  23610  reeff1o  26364  relogbcxpb  26704  logbgcd1irr  26711  fsumdvdsmul  27112  zabsle1  27214  2lgslem1c  27311  2lgsoddprmlem3  27332  2sq2  27351  2sqreultlem  27365  2sqreunnltlem  27368  2sqreulem3  27371  pntrlog2bndlem5  27499  sltlend  27690  upgrpredgv  29073  usgredg2vlem2  29160  ushgredgedg  29163  ushgredgedgloop  29165  uhgrspan1  29237  nb3grprlem1  29314  uvtxnbgrb  29335  cusgrsize2inds  29388  1egrvtxdg0  29446  uspgrloopvtxel  29451  finsumvtxdg2size  29485  rusgrpropnb  29518  ifpsnprss  29558  upgrwlkvtxedg  29580  uspgr2wlkeq  29581  wlkp1lem5  29612  wlkp1  29616  usgr2pth  29701  uspgrn2crct  29745  iswwlksnon  29790  wlkiswwlks1  29804  wlkiswwlks2lem3  29808  wwlksnextbi  29831  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  wwlksnextsurj  29837  wwlksnextprop  29849  wspn0  29861  umgr2adedgwlkonALT  29884  umgr2adedgspth  29885  umgr2wlkon  29887  elwwlks2ons3  29892  elwwlks2on  29896  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlkf1lem3  29942  clwwlkfo  29986  eleclclwwlknlem2  29997  erclwwlkntr  30007  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  0wlkonlem1  30054  upgr1wlkdlem1  30081  1pthon2v  30089  upgr3v3e3cycl  30116  uhgr3cyclexlem  30117  upgr4cycl4dv4e  30121  eupth2lem3lem3  30166  eupth2lem3lem4  30167  1to2vfriswmgr  30215  frgrncvvdeqlem6  30240  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  frgrwopreglem2  30249  2clwwlk2clwwlk  30286  extwwlkfab  30288  numclwwlk1lem2f1  30293  numclwwlkovh  30309  numclwwlk2lem1  30312  numclwlk2lem2f  30313  cdj1i  32369  brabgaf  32543  br8d  32545  sgn3da  32766  onvf1odlem1  35097  spthcycl  35123  goalrlem  35390  goalr  35391  fmlasucdisj  35393  satffunlem  35395  satffunlem1lem1  35396  satffunlem1lem2  35397  satffunlem2lem1  35398  satffunlem2lem2  35400  mthmb  35575  br8  35750  br4  35752  bj-snsetex  36958  bj-snglc  36964  copsex2d  37134  poimirlem20  37641  poimirlem26  37647  poimirlem27  37648  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  indexdom  37735  ismgmOLD  37851  rngodm1dm2  37933  rngomndo  37936  rngoueqz  37941  zerdivemp1x  37948  opcon3b  39196  ps-1  39478  3atlem5  39488  4atex  40077  selvvvval  42580  prjspvs  42605  iscard4  43529  pr2cv  43544  pm13.192  44406  iotavalsb  44429  relpfrlem  44950  fourierdlem32  46144  fourierdlem49  46160  fourierdlem64  46175  elprneb  47034  fveqvfvv  47045  funressnfv  47048  f1cof1b  47082  nvelim  47128  afvpcfv0  47151  afv0nbfvbi  47156  fnbrafvb  47159  tz6.12-afv  47178  afvco2  47181  ndmaovg  47189  afv2orxorb  47233  tz6.12-afv2  47245  tz6.12i-afv2  47248  f1oresf1o2  47296  elsetpreimafvbi  47396  imasetpreimafvbijlemfo  47410  iccpartiltu  47427  fargshiftfv  47444  fargshiftf  47445  lswn0  47449  prsprel  47492  reupr  47527  2exopprim  47530  fmtnorec2lem  47547  2pwp1prm  47594  lighneallem2  47611  lighneallem3  47612  proththd  47619  nn0o1gt2ALTV  47699  evenltle  47722  sbgoldbwt  47782  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  clnbgrval  47827  dfvopnbgr2  47857  uhgrimedgi  47894  gricushgr  47921  clnbgrgrim  47938  grimedg  47939  cycl3grtri  47950  isubgr3stgrlem4  47972  uspgrlimlem1  47991  grlimgrtri  47999  gpgedg2ov  48061  gpgedg2iv  48062  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  uspgropssxp  48136  lmod0rng  48221  lidldomn1  48223  zlidlring  48226  rngcinvALTV  48268  ztprmneprm  48339  lincext3  48449  zlmodzxznm  48490  suppdm  48503  elfzolborelfzop1  48512  nn0sumshdiglemB  48613  itcovalsucov  48661  lines  48724  rrx2vlinest  48734  line2xlem  48746  itschlc0yqe  48753  itsclquadeu  48770