Theorem eqcoms 2744

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 2743	. 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 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  gencbvex  3499  sbceq2a  3752  eqimss2  3993  uneqdifeq  4445  tppreq3  4716  ifpprsnss  4721  tpprceq3  4760  preqsnd  4815  prproe  4861  copsex2t  5440  snopeqop  5454  opthhausdorff0  5466  optocl  5718  relopabi  5771  cnvimassrndm  6110  cnveqb  6154  cnveq0  6155  unixpid  6242  reuop  6251  f0rn0  6719  fimadmfo  6755  f1ssf1  6806  tz6.12i  6860  fveqdmss  7023  fvcofneq  7038  funopsn  7093  f1ocnvfv  7224  f1ocnvfvb  7225  cbvfo  7235  riotaeqimp  7341  ov6g  7522  tfindsg  7803  findsg  7839  mptcnfimad  7930  suppimacnv  8116  ectocld  8719  ecoptocl  8744  undifixp  8872  f1dmvrnfibi  9241  f1vrnfibi  9242  updjud  9846  card1  9880  prdom2  9916  sornom  10187  indpi  10818  ltlen  11234  eqlei  11243  squeeze0  12045  nn0ind-raph  12592  fzoopth  13678  injresinjlem  13706  fvf1tp  13709  modmuladd  13836  modmuladdnn0  13838  hashf1rn  14275  hashrabsn1  14297  hash1snb  14342  hashgt12el  14345  hashgt12el2  14346  hashfzp1  14354  hash2prde  14393  hash2pwpr  14399  fi1uzind  14430  brfi1indALT  14433  lswlgt0cl  14492  wrd2ind  14646  pfxccatin12lem2  14654  pfxccatin12lem3  14655  cshweqrep  14744  scshwfzeqfzo  14749  cshimadifsn  14752  cshimadifsn0  14753  2swrd2eqwrdeq  14876  wwlktovfo  14881  rennim  15162  absmod0  15226  modfsummods  15716  mod2eq1n2dvds  16274  m1expe  16301  m1expo  16302  m1exp1  16303  nn0o1gt2  16308  flodddiv4  16342  cncongr1  16594  ge2nprmge4  16628  m1dvdsndvds  16726  cshwrepswhash1  17030  initoeu2lem1  17938  istos  18339  mgmsscl  18570  mndinvmod  18689  smndex1n0mnd  18837  symgfvne  19310  symgfix2  19345  symgextf1  19350  symgfixelsi  19364  psgnsn  19449  odbezout  19487  cntzcmnss  19770  frgpnabllem1  19802  ringinvnzdiv  20236  rngcinv  20570  psgndiflemB  21555  uvcendim  21802  mamufacex  22340  smatvscl  22468  mavmulsolcl  22495  mdetunilem8  22563  pm2mpfo  22758  chpscmat  22786  chmaidscmat  22792  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  txcn  23570  qtopeu  23660  reeff1o  26413  relogbcxpb  26753  logbgcd1irr  26760  fsumdvdsmul  27161  zabsle1  27263  2lgslem1c  27360  2lgsoddprmlem3  27381  2sq2  27400  2sqreultlem  27414  2sqreunnltlem  27417  2sqreulem3  27420  pntrlog2bndlem5  27548  ltlesnd  27743  upgrpredgv  29212  usgredg2vlem2  29299  ushgredgedg  29302  ushgredgedgloop  29304  uhgrspan1  29376  nb3grprlem1  29453  uvtxnbgrb  29474  cusgrsize2inds  29527  1egrvtxdg0  29585  uspgrloopvtxel  29590  finsumvtxdg2size  29624  rusgrpropnb  29657  ifpsnprss  29696  upgrwlkvtxedg  29718  uspgr2wlkeq  29719  wlkp1lem5  29749  wlkp1  29753  usgr2pth  29837  uspgrn2crct  29881  iswwlksnon  29926  wlkiswwlks1  29940  wlkiswwlks2lem3  29944  wwlksnextbi  29967  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  wwlksnextsurj  29973  wwlksnextprop  29985  wspn0  29997  umgr2adedgwlkonALT  30020  umgr2adedgspth  30021  umgr2wlkon  30023  elwwlks2ons3  30028  elwwlks2on  30034  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlkf1lem3  30081  clwwlkfo  30125  eleclclwwlknlem2  30136  erclwwlkntr  30146  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  0wlkonlem1  30193  upgr1wlkdlem1  30220  1pthon2v  30228  upgr3v3e3cycl  30255  uhgr3cyclexlem  30256  upgr4cycl4dv4e  30260  eupth2lem3lem3  30305  eupth2lem3lem4  30306  1to2vfriswmgr  30354  frgrncvvdeqlem6  30379  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  frgrwopreglem2  30388  2clwwlk2clwwlk  30425  extwwlkfab  30427  numclwwlk1lem2f1  30432  numclwwlkovh  30448  numclwwlk2lem1  30451  numclwlk2lem2f  30452  cdj1i  32508  brabgaf  32684  br8d  32686  sgn3da  32915  onvf1odlem1  35297  spthcycl  35323  goalrlem  35590  goalr  35591  fmlasucdisj  35593  satffunlem  35595  satffunlem1lem1  35596  satffunlem1lem2  35597  satffunlem2lem1  35598  satffunlem2lem2  35600  mthmb  35775  br8  35950  br4  35952  bj-snsetex  37164  bj-snglc  37170  copsex2d  37340  poimirlem20  37837  poimirlem26  37843  poimirlem27  37844  mblfinlem3  37856  mblfinlem4  37857  itg2addnclem  37868  indexdom  37931  ismgmOLD  38047  rngodm1dm2  38129  rngomndo  38132  rngoueqz  38137  zerdivemp1x  38144  opcon3b  39452  ps-1  39733  3atlem5  39743  4atex  40332  selvvvval  42824  prjspvs  42849  iscard4  43770  pr2cv  43785  pm13.192  44647  iotavalsb  44670  relpfrlem  45190  fourierdlem32  46379  fourierdlem49  46395  fourierdlem64  46410  elprneb  47271  fveqvfvv  47282  funressnfv  47285  f1cof1b  47319  nvelim  47365  afvpcfv0  47388  afv0nbfvbi  47393  fnbrafvb  47396  tz6.12-afv  47415  afvco2  47418  ndmaovg  47426  afv2orxorb  47470  tz6.12-afv2  47482  tz6.12i-afv2  47485  f1oresf1o2  47533  elsetpreimafvbi  47633  imasetpreimafvbijlemfo  47647  iccpartiltu  47664  fargshiftfv  47681  fargshiftf  47682  lswn0  47686  prsprel  47729  reupr  47764  2exopprim  47767  fmtnorec2lem  47784  2pwp1prm  47831  lighneallem2  47848  lighneallem3  47849  proththd  47856  nn0o1gt2ALTV  47936  evenltle  47959  sbgoldbwt  48019  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  clnbgrval  48064  dfvopnbgr2  48095  uhgrimedgi  48132  gricushgr  48159  clnbgrgrim  48176  grimedg  48177  cycl3grtri  48189  isubgr3stgrlem4  48211  uspgrlimlem1  48230  grlimgrtri  48245  gpgedg2ov  48308  gpgedg2iv  48309  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem2  48359  pgnbgreunbgrlem4  48361  uspgropssxp  48386  lmod0rng  48471  lidldomn1  48473  zlidlring  48476  rngcinvALTV  48518  ztprmneprm  48589  lincext3  48698  zlmodzxznm  48739  suppdm  48752  elfzolborelfzop1  48761  nn0sumshdiglemB  48862  itcovalsucov  48910  lines  48973  rrx2vlinest  48983  line2xlem  48995  itschlc0yqe  49002  itsclquadeu  49019