Theorem eqcoms 2769

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  gencbvex  3509  sbceq2a  3756  eqimss2  3995  uneqdifeq  4445  tppreq3  4717  ifpprsnss  4722  tpprceq3  4763  preqsnd  4816  prproe  4862  copsex2t  5460  snopeqop  5474  opthhausdorff0  5486  optocl  5739  relopabi  5793  cnvimassrndm  6134  cnveqb  6179  cnveq0  6180  unixpid  6267  reuop  6276  f0rn0  6745  fimadmfo  6783  f1ssf1  6835  tz6.12i  6889  fveqdmss  7055  fvcofneq  7070  funopsnOLD  7127  f1ocnvfv  7258  f1ocnvfvb  7259  cbvfo  7269  riotaeqimp  7375  ov6g  7556  tfindsg  7837  findsg  7874  mptcnfimad  7963  suppimacnv  8149  ectocld  8759  ecoptocl  8784  undifixp  8912  f1dmvrnfibi  9281  f1vrnfibi  9282  updjud  9889  card1  9923  prdom2  9959  sornom  10231  indpi  10862  ltlen  11281  eqlei  11290  squeeze0  12092  nn0ind-raph  12670  fzoopth  13765  injresinjlem  13793  fvf1tp  13796  modmuladd  13923  modmuladdnn0  13925  hashf1rn  14362  hashrabsn1  14384  hash1snb  14429  hashgt12el  14432  hashgt12el2  14433  hashfzp1  14441  hash2prde  14480  hash2pwpr  14486  fi1uzind  14517  brfi1indALT  14520  lswlgt0cl  14579  wrd2ind  14733  pfxccatin12lem2  14741  pfxccatin12lem3  14742  cshweqrep  14831  scshwfzeqfzo  14836  cshimadifsn  14839  cshimadifsn0  14840  2swrd2eqwrdeq  14963  wwlktovfo  14968  rennim  15249  absmod0  15313  modfsummods  15804  mod2eq1n2dvds  16364  m1expe  16391  m1expo  16392  m1exp1  16393  nn0o1gt2  16398  flodddiv4  16432  cncongr1  16684  ge2nprmge4  16719  m1dvdsndvds  16817  cshwrepswhash1  17121  initoeu2lem1  18030  istos  18431  mgmsscl  18662  mndinvmod  18781  smndex1n0mnd  18932  symgfvne  19404  symgfix2  19439  symgextf1  19444  symgfixelsi  19458  psgnsn  19543  odbezout  19581  cntzcmnss  19864  frgpnabllem1  19896  ringinvnzdiv  20330  rngcinv  20666  psgndiflemB  21632  uvcendim  21879  selvvvval  22175  mamufacex  22436  smatvscl  22564  mavmulsolcl  22591  mdetunilem8  22659  pm2mpfo  22854  chpscmat  22882  chmaidscmat  22888  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  txcn  23666  qtopeu  23756  reeff1o  26487  relogbcxpb  26829  logbgcd1irr  26836  fsumdvdsmul  27236  zabsle1  27337  2lgslem1c  27434  2lgsoddprmlem3  27455  2sq2  27474  2sqreultlem  27488  2sqreunnltlem  27491  2sqreulem3  27494  pntrlog2bndlem5  27622  ltlesnd  27816  upgrpredgv  29286  usgredg2vlem2  29373  ushgredgedg  29376  ushgredgedgloop  29378  uhgrspan1  29450  nb3grprlem1  29527  uvtxnbgrb  29548  cusgrsize2inds  29600  1egrvtxdg0  29658  uspgrloopvtxel  29663  finsumvtxdg2size  29697  rusgrpropnb  29730  ifpsnprss  29769  upgrwlkvtxedg  29791  uspgr2wlkeq  29792  wlkp1lem5  29822  wlkp1  29826  usgr2pth  29910  uspgrn2crct  29954  iswwlksnon  29999  wlkiswwlks1  30013  wlkiswwlks2lem3  30017  wwlksnextbi  30040  wwlksnredwwlkn0  30042  wwlksnextwrd  30043  wwlksnextsurj  30046  wwlksnextprop  30058  wspn0  30070  umgr2adedgwlkonALT  30093  umgr2adedgspth  30094  umgr2wlkon  30096  elwwlks2ons3  30101  elwwlks2on  30107  clwlkclwwlklem2a4  30145  clwlkclwwlklem2a  30146  clwlkclwwlkf1lem3  30154  clwwlkfo  30198  eleclclwwlknlem2  30209  erclwwlkntr  30219  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  0wlkonlem1  30266  upgr1wlkdlem1  30293  1pthon2v  30301  upgr3v3e3cycl  30328  uhgr3cyclexlem  30329  upgr4cycl4dv4e  30333  eupth2lem3lem3  30378  eupth2lem3lem4  30379  1to2vfriswmgr  30427  frgrncvvdeqlem6  30452  frgrncvvdeqlem8  30454  frgrncvvdeqlem9  30455  frgrwopreglem2  30461  2clwwlk2clwwlk  30498  extwwlkfab  30500  numclwwlk1lem2f1  30505  numclwwlkovh  30521  numclwwlk2lem1  30524  numclwlk2lem2f  30525  cdj1i  32582  brabgaf  32758  br8d  32760  sgn3da  32986  onvf1odlem1  35410  spthcycl  35443  goalrlem  35710  goalr  35711  fmlasucdisj  35713  satffunlem  35715  satffunlem1lem1  35716  satffunlem1lem2  35717  satffunlem2lem1  35718  satffunlem2lem2  35720  mthmb  35895  br8  36070  br4  36072  bj-snsetex  37412  bj-snglc  37418  copsex2d  37595  wl-dfcleq  37972  poimirlem20  38103  poimirlem26  38109  poimirlem27  38110  mblfinlem3  38122  mblfinlem4  38123  itg2addnclem  38134  indexdom  38197  ismgmOLD  38313  rngodm1dm2  38395  rngomndo  38398  rngoueqz  38403  zerdivemp1x  38410  opcon3b  39784  ps-1  40065  3atlem5  40075  4atex  40664  prjspvs  43156  iscard4  44073  pr2cv  44088  pm13.192  44950  iotavalsb  44973  relpfrlem  45493  fourierdlem32  46677  fourierdlem49  46693  fourierdlem64  46708  elprneb  47587  fveqvfvv  47598  funressnfv  47601  f1cof1b  47635  nvelim  47681  afvpcfv0  47704  afv0nbfvbi  47709  fnbrafvb  47712  tz6.12-afv  47731  afvco2  47734  ndmaovg  47742  afv2orxorb  47786  tz6.12-afv2  47798  tz6.12i-afv2  47801  f1oresf1o2  47849  nnmul2  47888  elsetpreimafvbi  47961  imasetpreimafvbijlemfo  47975  iccpartiltu  47992  fargshiftfv  48009  fargshiftf  48010  lswn0  48014  prsprel  48057  reupr  48092  2exopprim  48095  fmtnorec2lem  48115  2pwp1prm  48162  lighneallem2  48179  lighneallem3  48180  proththd  48187  ppivalnnprm  48198  ppivalnnnprmge6  48199  nn0o1gt2ALTV  48280  evenltle  48303  sbgoldbwt  48363  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  clnbgrval  48408  dfvopnbgr2  48439  uhgrimedgi  48476  gricushgr  48503  clnbgrgrim  48520  grimedg  48521  cycl3grtri  48533  isubgr3stgrlem4  48555  uspgrlimlem1  48574  grlimgrtri  48589  gpgedg2ov  48652  gpgedg2iv  48653  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem2  48703  pgnbgreunbgrlem4  48705  uspgropssxp  48730  lmod0rng  48815  lidldomn1  48817  zlidlring  48820  rngcinvALTV  48862  ztprmneprm  48933  lincext3  49042  zlmodzxznm  49083  suppdm  49096  elfzolborelfzop1  49105  nn0sumshdiglemB  49206  itcovalsucov  49254  lines  49317  rrx2vlinest  49327  line2xlem  49339  itschlc0yqe  49346  itsclquadeu  49363