Theorem eqcoms 2745

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 2744	. 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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  gencbvex  3541  sbceq2a  3800  eqimss2  4043  uneqdifeq  4493  tppreq3  4759  ifpprsnss  4764  tpprceq3  4804  preqsnd  4859  prproe  4905  copsex2t  5497  snopeqop  5511  opthhausdorff0  5523  relopabi  5832  cnvimassrndm  6172  cnveqb  6216  cnveq0  6217  unixpid  6304  reuop  6313  f0rn0  6793  fimadmfo  6829  f1ssf1  6880  tz6.12i  6934  fveqdmss  7098  fvcofneq  7113  funopsn  7168  f1ocnvfv  7298  f1ocnvfvb  7299  cbvfo  7309  riotaeqimp  7414  ov6g  7597  tfindsg  7882  findsg  7919  mptcnfimad  8011  suppimacnv  8199  ectocld  8824  ecoptocl  8847  undifixp  8974  phplem3OLD  9256  f1dmvrnfibi  9381  f1vrnfibi  9382  updjud  9974  card1  10008  pr2neOLD  10045  prdom2  10046  sornom  10317  indpi  10947  ltlen  11362  eqlei  11371  squeeze0  12171  nn0ind-raph  12718  fzoopth  13801  injresinjlem  13826  fvf1tp  13829  modmuladd  13954  modmuladdnn0  13956  hashf1rn  14391  hashrabsn1  14413  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hashfzp1  14470  hash2prde  14509  hash2pwpr  14515  fi1uzind  14546  brfi1indALT  14549  lswlgt0cl  14607  wrd2ind  14761  pfxccatin12lem2  14769  pfxccatin12lem3  14770  cshweqrep  14859  cshwsexaOLD  14863  scshwfzeqfzo  14865  cshimadifsn  14868  cshimadifsn0  14869  2swrd2eqwrdeq  14992  wwlktovfo  14997  rennim  15278  absmod0  15342  modfsummods  15829  mod2eq1n2dvds  16384  m1expe  16411  m1expo  16412  m1exp1  16413  nn0o1gt2  16418  flodddiv4  16452  cncongr1  16704  ge2nprmge4  16738  m1dvdsndvds  16836  cshwrepswhash1  17140  initoeu2lem1  18059  istos  18463  mgmsscl  18658  mndinvmod  18777  smndex1n0mnd  18925  symgfvne  19398  symgfix2  19434  symgextf1  19439  symgfixelsi  19453  psgnsn  19538  odbezout  19576  cntzcmnss  19859  frgpnabllem1  19891  ringinvnzdiv  20298  rngcinv  20637  psgndiflemB  21618  uvcendim  21867  mamufacex  22400  smatvscl  22530  mavmulsolcl  22557  mdetunilem8  22625  pm2mpfo  22820  chpscmat  22848  chmaidscmat  22854  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  txcn  23634  qtopeu  23724  reeff1o  26491  relogbcxpb  26830  logbgcd1irr  26837  fsumdvdsmul  27238  zabsle1  27340  2lgslem1c  27437  2lgsoddprmlem3  27458  2sq2  27477  2sqreultlem  27491  2sqreunnltlem  27494  2sqreulem3  27497  pntrlog2bndlem5  27625  sltlend  27816  upgrpredgv  29156  usgredg2vlem2  29243  ushgredgedg  29246  ushgredgedgloop  29248  uhgrspan1  29320  nb3grprlem1  29397  uvtxnbgrb  29418  cusgrsize2inds  29471  1egrvtxdg0  29529  uspgrloopvtxel  29534  finsumvtxdg2size  29568  rusgrpropnb  29601  ifpsnprss  29641  upgrwlkvtxedg  29663  uspgr2wlkeq  29664  wlkp1lem5  29695  wlkp1  29699  usgr2pth  29784  uspgrn2crct  29828  iswwlksnon  29873  wlkiswwlks1  29887  wlkiswwlks2lem3  29891  wwlksnextbi  29914  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  wwlksnextsurj  29920  wwlksnextprop  29932  wspn0  29944  umgr2adedgwlkonALT  29967  umgr2adedgspth  29968  umgr2wlkon  29970  elwwlks2ons3  29975  elwwlks2on  29979  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlkf1lem3  30025  clwwlkfo  30069  eleclclwwlknlem2  30080  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  0wlkonlem1  30137  upgr1wlkdlem1  30164  1pthon2v  30172  upgr3v3e3cycl  30199  uhgr3cyclexlem  30200  upgr4cycl4dv4e  30204  eupth2lem3lem3  30249  eupth2lem3lem4  30250  1to2vfriswmgr  30298  frgrncvvdeqlem6  30323  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrwopreglem2  30332  2clwwlk2clwwlk  30369  extwwlkfab  30371  numclwwlk1lem2f1  30376  numclwwlkovh  30392  numclwwlk2lem1  30395  numclwlk2lem2f  30396  cdj1i  32452  brabgaf  32620  br8d  32622  sgn3da  34544  spthcycl  35134  goalrlem  35401  goalr  35402  fmlasucdisj  35404  satffunlem  35406  satffunlem1lem1  35407  satffunlem1lem2  35408  satffunlem2lem1  35409  satffunlem2lem2  35411  mthmb  35586  br8  35756  br4  35758  bj-snsetex  36964  bj-snglc  36970  copsex2d  37140  poimirlem20  37647  poimirlem26  37653  poimirlem27  37654  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  indexdom  37741  ismgmOLD  37857  rngodm1dm2  37939  rngomndo  37942  rngoueqz  37947  zerdivemp1x  37954  opcon3b  39197  ps-1  39479  3atlem5  39489  4atex  40078  selvvvval  42595  prjspvs  42620  iscard4  43546  pr2cv  43561  pm13.192  44429  iotavalsb  44452  relpfrlem  44974  fourierdlem32  46154  fourierdlem49  46170  fourierdlem64  46185  elprneb  47041  fveqvfvv  47052  funressnfv  47055  f1cof1b  47089  nvelim  47135  afvpcfv0  47158  afv0nbfvbi  47163  fnbrafvb  47166  tz6.12-afv  47185  afvco2  47188  ndmaovg  47196  afv2orxorb  47240  tz6.12-afv2  47252  tz6.12i-afv2  47255  f1oresf1o2  47303  elsetpreimafvbi  47378  imasetpreimafvbijlemfo  47392  iccpartiltu  47409  fargshiftfv  47426  fargshiftf  47427  lswn0  47431  prsprel  47474  reupr  47509  2exopprim  47512  fmtnorec2lem  47529  2pwp1prm  47576  lighneallem2  47593  lighneallem3  47594  proththd  47601  nn0o1gt2ALTV  47681  evenltle  47704  sbgoldbwt  47764  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  clnbgrval  47809  dfvopnbgr2  47839  gricushgr  47886  clnbgrgrim  47902  grimedg  47903  cycl3grtri  47914  isubgr3stgrlem4  47936  uspgrlimlem1  47955  grlimgrtri  47963  uspgropssxp  48060  lmod0rng  48145  lidldomn1  48147  zlidlring  48150  rngcinvALTV  48192  ztprmneprm  48263  lincext3  48373  zlmodzxznm  48414  suppdm  48427  elfzolborelfzop1  48436  nn0sumshdiglemB  48541  itcovalsucov  48589  lines  48652  rrx2vlinest  48662  line2xlem  48674  itschlc0yqe  48681  itsclquadeu  48698