Theorem eqcoms 2770

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  gencbvex  3510  sbceq2a  3755  eqimss2  3995  uneqdifeq  4452  tppreq3  4724  ifpprsnss  4729  tpprceq3  4771  preqsnd  4823  prproe  4869  copsex2t  5474  snopeqop  5488  opthhausdorff0  5500  optocl  5754  relopabi  5808  cnvimassrndm  6148  cnveqb  6194  cnveq0  6195  unixpid  6285  reuop  6294  f0rn0  6763  fimadmfo  6801  f1ssf1  6853  tz6.12i  6907  fveqdmss  7073  fvcofneq  7088  funopsnOLD  7145  f1ocnvfv  7276  f1ocnvfvb  7277  cbvfo  7287  riotaeqimp  7395  ov6g  7576  tfindsg  7855  findsg  7892  mptcnfimad  7981  suppimacnv  8168  ectocld  8778  ecoptocl  8803  undifixp  8930  f1dmvrnfibi  9296  f1vrnfibi  9297  updjud  9927  card1  9961  prdom2  9997  sornom  10267  indpi  10898  ltlen  11317  eqlei  11326  squeeze0  12124  nn0ind-raph  12702  fzoopth  13798  injresinjlem  13826  fvf1tp  13829  modmuladd  13956  modmuladdnn0  13958  hashf1rn  14395  hashrabsn1  14417  hash1snb  14463  hashgt12el  14466  hashgt12el2  14467  hashfzp1  14475  hash2prde  14514  hash2pwpr  14520  fi1uzind  14551  brfi1indALT  14554  lswlgt0cl  14613  wrd2ind  14767  pfxccatin12lem2  14775  pfxccatin12lem3  14776  cshweqrep  14865  scshwfzeqfzo  14870  cshimadifsn  14873  cshimadifsn0  14874  2swrd2eqwrdeq  14997  wwlktovfo  15002  sgn3da  15145  rennim  15297  absmod0  15361  modfsummods  15852  mod2eq1n2dvds  16411  m1expe  16438  m1expo  16439  m1exp1  16440  nn0o1gt2  16445  flodddiv4  16479  cncongr1  16731  ge2nprmge4  16766  m1dvdsndvds  16864  cshwrepswhash1  17168  initoeu2lem1  18077  istos  18478  mgmsscl  18709  mndinvmod  18828  smndex1n0mnd  18980  symgfvne  19457  symgfix2  19492  symgextf1  19497  symgfixelsi  19511  psgnsn  19596  odbezout  19634  cntzcmnss  19917  frgpnabllem1  19949  ringinvnzdiv  20391  rngcinv  20747  psgndiflemB  21761  uvcendim  22008  selvvvval  22304  mamufacex  22564  smatvscl  22692  mavmulsolcl  22719  mdetunilem8  22787  pm2mpfo  22982  chpscmat  23010  chmaidscmat  23016  chfacfscmulgsum  23028  chfacfpmmulgsum  23032  txcn  23794  qtopeu  23884  reeff1o  26621  relogbcxpb  26963  logbgcd1irr  26970  fsumdvdsmul  27370  zabsle1  27471  2lgslem1c  27568  2lgsoddprmlem3  27589  2sq2  27608  2sqreultlem  27622  2sqreunnltlem  27625  2sqreulem3  27628  pntrlog2bndlem5  27756  ltlesnd  27950  upgrpredgv  29500  usgredg2vlem2  29587  ushgredgedg  29590  ushgredgedgloop  29592  uhgrspan1  29664  nb3grprlem1  29741  uvtxnbgrb  29762  cusgrsize2inds  29814  1egrvtxdg0  29872  uspgrloopvtxel  29877  finsumvtxdg2size  29911  rusgrpropnb  29944  ifpsnprss  29983  upgrwlkvtxedg  30005  uspgr2wlkeq  30006  wlkp1lem5  30036  wlkp1  30040  usgr2pth  30124  uspgrn2crct  30168  iswwlksnon  30213  wlkiswwlks1  30227  wlkiswwlks2lem3  30231  wwlksnextbi  30254  wwlksnredwwlkn0  30256  wwlksnextwrd  30257  wwlksnextsurj  30260  wwlksnextprop  30272  wspn0  30284  umgr2adedgwlkonALT  30307  umgr2adedgspth  30308  umgr2wlkon  30310  elwwlks2ons3  30315  elwwlks2on  30321  clwlkclwwlklem2a4  30359  clwlkclwwlklem2a  30360  clwlkclwwlkf1lem3  30368  clwwlkfo  30412  eleclclwwlknlem2  30423  erclwwlkntr  30433  hashecclwwlkn1  30439  umgrhashecclwwlk  30440  0wlkonlem1  30480  upgr1wlkdlem1  30507  1pthon2v  30515  upgr3v3e3cycl  30542  uhgr3cyclexlem  30543  upgr4cycl4dv4e  30547  eupth2lem3lem3  30592  eupth2lem3lem4  30593  1to2vfriswmgr  30641  frgrncvvdeqlem6  30666  frgrncvvdeqlem8  30668  frgrncvvdeqlem9  30669  frgrwopreglem2  30675  2clwwlk2clwwlk  30712  extwwlkfab  30714  numclwwlk1lem2f1  30719  numclwwlkovh  30735  numclwwlk2lem1  30738  numclwlk2lem2f  30739  cdj1i  32796  brabgaf  32962  br8d  32964  kardcard2b  35586  onvf1odlem1  35595  spthcycl  35629  goalrlem  35896  goalr  35897  fmlasucdisj  35899  satffunlem  35901  satffunlem1lem1  35902  satffunlem1lem2  35903  satffunlem2lem1  35904  satffunlem2lem2  35906  mthmb  36081  br8  36256  br4  36258  bj-snsetex  37627  bj-snglc  37633  copsex2d  37811  wl-dfcleq  38188  poimirlem20  38319  poimirlem26  38325  poimirlem27  38326  mblfinlem3  38338  mblfinlem4  38339  itg2addnclem  38350  indexdom  38413  ismgmOLD  38529  rngodm1dm2  38611  rngomndo  38614  rngoueqz  38619  zerdivemp1x  38626  opcon3b  39998  ps-1  40279  3atlem5  40289  4atex  40878  prjspvs  43370  iscard4  44287  pr2cv  44302  pm13.192  45148  iotavalsb  45171  relpfrlem  45690  fourierdlem32  46881  fourierdlem49  46897  fourierdlem64  46912  elprneb  47794  fveqvfvv  47805  funressnfv  47808  f1cof1b  47842  nvelim  47888  afvpcfv0  47911  afv0nbfvbi  47916  fnbrafvb  47919  tz6.12-afv  47938  afvco2  47941  ndmaovg  47949  afv2orxorb  47993  tz6.12-afv2  48005  tz6.12i-afv2  48008  f1oresf1o2  48056  nnmul2  48095  elsetpreimafvbi  48168  imasetpreimafvbijlemfo  48182  iccpartiltu  48199  fargshiftfv  48216  fargshiftf  48217  lswn0  48221  prsprel  48264  reupr  48299  2exopprim  48302  fmtnorec2lem  48322  2pwp1prm  48369  lighneallem2  48386  lighneallem3  48387  proththd  48394  ppivalnnprm  48405  ppivalnnnprmge6  48406  nn0o1gt2ALTV  48487  evenltle  48510  sbgoldbwt  48570  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  clnbgrval  48615  dfvopnbgr2  48646  uhgrimedgi  48683  gricushgr  48710  clnbgrgrim  48727  grimedg  48728  cycl3grtri  48740  isubgr3stgrlem4  48762  uspgrlimlem1  48781  grlimgrtri  48796  gpgedg2ov  48859  gpgedg2iv  48860  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem2lem3  48909  pgnbgreunbgrlem2  48910  pgnbgreunbgrlem4  48912  uspgropssxp  48937  lmod0rng  49022  lidldomn1  49024  zlidlring  49027  rngcinvALTV  49069  ztprmneprm  49155  lincext3  49264  zlmodzxznm  49305  suppdm  49318  elfzolborelfzop1  49327  nn0sumshdiglemB  49428  itcovalsucov  49476  lines  49539  rrx2vlinest  49549  line2xlem  49561  itschlc0yqe  49568  itsclquadeu  49585