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  3496  sbceq2a  3753  eqimss2  3994  uneqdifeq  4443  tppreq3  4712  ifpprsnss  4717  tpprceq3  4756  preqsnd  4811  prproe  4857  copsex2t  5432  snopeqop  5446  opthhausdorff0  5458  optocl  5710  relopabi  5762  cnvimassrndm  6099  cnveqb  6143  cnveq0  6144  unixpid  6231  reuop  6240  f0rn0  6708  fimadmfo  6744  f1ssf1  6795  tz6.12i  6848  fveqdmss  7011  fvcofneq  7026  funopsn  7081  f1ocnvfv  7212  f1ocnvfvb  7213  cbvfo  7223  riotaeqimp  7329  ov6g  7510  tfindsg  7791  findsg  7827  mptcnfimad  7918  suppimacnv  8104  ectocld  8706  ecoptocl  8731  undifixp  8858  f1dmvrnfibi  9225  f1vrnfibi  9226  updjud  9824  card1  9858  prdom2  9894  sornom  10165  indpi  10795  ltlen  11211  eqlei  11220  squeeze0  12022  nn0ind-raph  12570  fzoopth  13659  injresinjlem  13687  fvf1tp  13690  modmuladd  13817  modmuladdnn0  13819  hashf1rn  14256  hashrabsn1  14278  hash1snb  14323  hashgt12el  14326  hashgt12el2  14327  hashfzp1  14335  hash2prde  14374  hash2pwpr  14380  fi1uzind  14411  brfi1indALT  14414  lswlgt0cl  14473  wrd2ind  14627  pfxccatin12lem2  14635  pfxccatin12lem3  14636  cshweqrep  14725  scshwfzeqfzo  14730  cshimadifsn  14733  cshimadifsn0  14734  2swrd2eqwrdeq  14857  wwlktovfo  14862  rennim  15143  absmod0  15207  modfsummods  15697  mod2eq1n2dvds  16255  m1expe  16282  m1expo  16283  m1exp1  16284  nn0o1gt2  16289  flodddiv4  16323  cncongr1  16575  ge2nprmge4  16609  m1dvdsndvds  16707  cshwrepswhash1  17011  initoeu2lem1  17918  istos  18319  mgmsscl  18550  mndinvmod  18669  smndex1n0mnd  18817  symgfvne  19291  symgfix2  19326  symgextf1  19331  symgfixelsi  19345  psgnsn  19430  odbezout  19468  cntzcmnss  19751  frgpnabllem1  19783  ringinvnzdiv  20217  rngcinv  20550  psgndiflemB  21535  uvcendim  21782  mamufacex  22309  smatvscl  22437  mavmulsolcl  22464  mdetunilem8  22532  pm2mpfo  22727  chpscmat  22755  chmaidscmat  22761  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  txcn  23539  qtopeu  23629  reeff1o  26382  relogbcxpb  26722  logbgcd1irr  26729  fsumdvdsmul  27130  zabsle1  27232  2lgslem1c  27329  2lgsoddprmlem3  27350  2sq2  27369  2sqreultlem  27383  2sqreunnltlem  27386  2sqreulem3  27389  pntrlog2bndlem5  27517  sltlend  27708  upgrpredgv  29115  usgredg2vlem2  29202  ushgredgedg  29205  ushgredgedgloop  29207  uhgrspan1  29279  nb3grprlem1  29356  uvtxnbgrb  29377  cusgrsize2inds  29430  1egrvtxdg0  29488  uspgrloopvtxel  29493  finsumvtxdg2size  29527  rusgrpropnb  29560  ifpsnprss  29599  upgrwlkvtxedg  29621  uspgr2wlkeq  29622  wlkp1lem5  29652  wlkp1  29656  usgr2pth  29740  uspgrn2crct  29784  iswwlksnon  29829  wlkiswwlks1  29843  wlkiswwlks2lem3  29847  wwlksnextbi  29870  wwlksnredwwlkn0  29872  wwlksnextwrd  29873  wwlksnextsurj  29876  wwlksnextprop  29888  wspn0  29900  umgr2adedgwlkonALT  29923  umgr2adedgspth  29924  umgr2wlkon  29926  elwwlks2ons3  29931  elwwlks2on  29935  clwlkclwwlklem2a4  29972  clwlkclwwlklem2a  29973  clwlkclwwlkf1lem3  29981  clwwlkfo  30025  eleclclwwlknlem2  30036  erclwwlkntr  30046  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  0wlkonlem1  30093  upgr1wlkdlem1  30120  1pthon2v  30128  upgr3v3e3cycl  30155  uhgr3cyclexlem  30156  upgr4cycl4dv4e  30160  eupth2lem3lem3  30205  eupth2lem3lem4  30206  1to2vfriswmgr  30254  frgrncvvdeqlem6  30279  frgrncvvdeqlem8  30281  frgrncvvdeqlem9  30282  frgrwopreglem2  30288  2clwwlk2clwwlk  30325  extwwlkfab  30327  numclwwlk1lem2f1  30332  numclwwlkovh  30348  numclwwlk2lem1  30351  numclwlk2lem2f  30352  cdj1i  32408  brabgaf  32584  br8d  32586  sgn3da  32812  onvf1odlem1  35135  spthcycl  35161  goalrlem  35428  goalr  35429  fmlasucdisj  35431  satffunlem  35433  satffunlem1lem1  35434  satffunlem1lem2  35435  satffunlem2lem1  35436  satffunlem2lem2  35438  mthmb  35613  br8  35788  br4  35790  bj-snsetex  36996  bj-snglc  37002  copsex2d  37172  poimirlem20  37679  poimirlem26  37685  poimirlem27  37686  mblfinlem3  37698  mblfinlem4  37699  itg2addnclem  37710  indexdom  37773  ismgmOLD  37889  rngodm1dm2  37971  rngomndo  37974  rngoueqz  37979  zerdivemp1x  37986  opcon3b  39234  ps-1  39515  3atlem5  39525  4atex  40114  selvvvval  42617  prjspvs  42642  iscard4  43565  pr2cv  43580  pm13.192  44442  iotavalsb  44465  relpfrlem  44985  fourierdlem32  46176  fourierdlem49  46192  fourierdlem64  46207  elprneb  47059  fveqvfvv  47070  funressnfv  47073  f1cof1b  47107  nvelim  47153  afvpcfv0  47176  afv0nbfvbi  47181  fnbrafvb  47184  tz6.12-afv  47203  afvco2  47206  ndmaovg  47214  afv2orxorb  47258  tz6.12-afv2  47270  tz6.12i-afv2  47273  f1oresf1o2  47321  elsetpreimafvbi  47421  imasetpreimafvbijlemfo  47435  iccpartiltu  47452  fargshiftfv  47469  fargshiftf  47470  lswn0  47474  prsprel  47517  reupr  47552  2exopprim  47555  fmtnorec2lem  47572  2pwp1prm  47619  lighneallem2  47636  lighneallem3  47637  proththd  47644  nn0o1gt2ALTV  47724  evenltle  47747  sbgoldbwt  47807  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  clnbgrval  47852  dfvopnbgr2  47883  uhgrimedgi  47920  gricushgr  47947  clnbgrgrim  47964  grimedg  47965  cycl3grtri  47977  isubgr3stgrlem4  47999  uspgrlimlem1  48018  grlimgrtri  48033  gpgedg2ov  48096  gpgedg2iv  48097  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem2  48147  pgnbgreunbgrlem4  48149  uspgropssxp  48174  lmod0rng  48259  lidldomn1  48261  zlidlring  48264  rngcinvALTV  48306  ztprmneprm  48377  lincext3  48487  zlmodzxznm  48528  suppdm  48541  elfzolborelfzop1  48550  nn0sumshdiglemB  48651  itcovalsucov  48699  lines  48762  rrx2vlinest  48772  line2xlem  48784  itschlc0yqe  48791  itsclquadeu  48808