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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  gencbvex  3488  sbceq2a  3741  eqimss2  3982  uneqdifeq  4433  tppreq3  4704  ifpprsnss  4709  tpprceq3  4748  preqsnd  4803  prproe  4849  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  7024  fvcofneq  7039  funopsn  7095  f1ocnvfv  7226  f1ocnvfvb  7227  cbvfo  7237  riotaeqimp  7343  ov6g  7524  tfindsg  7805  findsg  7841  mptcnfimad  7932  suppimacnv  8117  ectocld  8722  ecoptocl  8747  undifixp  8875  f1dmvrnfibi  9244  f1vrnfibi  9245  updjud  9849  card1  9883  prdom2  9919  sornom  10190  indpi  10821  ltlen  11238  eqlei  11247  squeeze0  12050  nn0ind-raph  12620  fzoopth  13708  injresinjlem  13736  fvf1tp  13739  modmuladd  13866  modmuladdnn0  13868  hashf1rn  14305  hashrabsn1  14327  hash1snb  14372  hashgt12el  14375  hashgt12el2  14376  hashfzp1  14384  hash2prde  14423  hash2pwpr  14429  fi1uzind  14460  brfi1indALT  14463  lswlgt0cl  14522  wrd2ind  14676  pfxccatin12lem2  14684  pfxccatin12lem3  14685  cshweqrep  14774  scshwfzeqfzo  14779  cshimadifsn  14782  cshimadifsn0  14783  2swrd2eqwrdeq  14906  wwlktovfo  14911  rennim  15192  absmod0  15256  modfsummods  15747  mod2eq1n2dvds  16307  m1expe  16334  m1expo  16335  m1exp1  16336  nn0o1gt2  16341  flodddiv4  16375  cncongr1  16627  ge2nprmge4  16662  m1dvdsndvds  16760  cshwrepswhash1  17064  initoeu2lem1  17972  istos  18373  mgmsscl  18604  mndinvmod  18723  smndex1n0mnd  18874  symgfvne  19347  symgfix2  19382  symgextf1  19387  symgfixelsi  19401  psgnsn  19486  odbezout  19524  cntzcmnss  19807  frgpnabllem1  19839  ringinvnzdiv  20273  rngcinv  20605  psgndiflemB  21590  uvcendim  21837  mamufacex  22371  smatvscl  22499  mavmulsolcl  22526  mdetunilem8  22594  pm2mpfo  22789  chpscmat  22817  chmaidscmat  22823  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  txcn  23601  qtopeu  23691  reeff1o  26425  relogbcxpb  26764  logbgcd1irr  26771  fsumdvdsmul  27172  zabsle1  27273  2lgslem1c  27370  2lgsoddprmlem3  27391  2sq2  27410  2sqreultlem  27424  2sqreunnltlem  27427  2sqreulem3  27430  pntrlog2bndlem5  27558  ltlesnd  27753  upgrpredgv  29222  usgredg2vlem2  29309  ushgredgedg  29312  ushgredgedgloop  29314  uhgrspan1  29386  nb3grprlem1  29463  uvtxnbgrb  29484  cusgrsize2inds  29537  1egrvtxdg0  29595  uspgrloopvtxel  29600  finsumvtxdg2size  29634  rusgrpropnb  29667  ifpsnprss  29706  upgrwlkvtxedg  29728  uspgr2wlkeq  29729  wlkp1lem5  29759  wlkp1  29763  usgr2pth  29847  uspgrn2crct  29891  iswwlksnon  29936  wlkiswwlks1  29950  wlkiswwlks2lem3  29954  wwlksnextbi  29977  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  wwlksnextsurj  29983  wwlksnextprop  29995  wspn0  30007  umgr2adedgwlkonALT  30030  umgr2adedgspth  30031  umgr2wlkon  30033  elwwlks2ons3  30038  elwwlks2on  30044  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlkf1lem3  30091  clwwlkfo  30135  eleclclwwlknlem2  30146  erclwwlkntr  30156  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  0wlkonlem1  30203  upgr1wlkdlem1  30230  1pthon2v  30238  upgr3v3e3cycl  30265  uhgr3cyclexlem  30266  upgr4cycl4dv4e  30270  eupth2lem3lem3  30315  eupth2lem3lem4  30316  1to2vfriswmgr  30364  frgrncvvdeqlem6  30389  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  frgrwopreglem2  30398  2clwwlk2clwwlk  30435  extwwlkfab  30437  numclwwlk1lem2f1  30442  numclwwlkovh  30458  numclwwlk2lem1  30461  numclwlk2lem2f  30462  cdj1i  32519  brabgaf  32694  br8d  32696  sgn3da  32922  onvf1odlem1  35301  spthcycl  35327  goalrlem  35594  goalr  35595  fmlasucdisj  35597  satffunlem  35599  satffunlem1lem1  35600  satffunlem1lem2  35601  satffunlem2lem1  35602  satffunlem2lem2  35604  mthmb  35779  br8  35954  br4  35956  bj-snsetex  37286  bj-snglc  37292  copsex2d  37469  wl-dfcleq  37844  poimirlem20  37975  poimirlem26  37981  poimirlem27  37982  mblfinlem3  37994  mblfinlem4  37995  itg2addnclem  38006  indexdom  38069  ismgmOLD  38185  rngodm1dm2  38267  rngomndo  38270  rngoueqz  38275  zerdivemp1x  38282  opcon3b  39656  ps-1  39937  3atlem5  39947  4atex  40536  selvvvval  43032  prjspvs  43057  iscard4  43978  pr2cv  43993  pm13.192  44855  iotavalsb  44878  relpfrlem  45398  fourierdlem32  46585  fourierdlem49  46601  fourierdlem64  46616  elprneb  47489  fveqvfvv  47500  funressnfv  47503  f1cof1b  47537  nvelim  47583  afvpcfv0  47606  afv0nbfvbi  47611  fnbrafvb  47614  tz6.12-afv  47633  afvco2  47636  ndmaovg  47644  afv2orxorb  47688  tz6.12-afv2  47700  tz6.12i-afv2  47703  f1oresf1o2  47751  nnmul2  47790  elsetpreimafvbi  47863  imasetpreimafvbijlemfo  47877  iccpartiltu  47894  fargshiftfv  47911  fargshiftf  47912  lswn0  47916  prsprel  47959  reupr  47994  2exopprim  47997  fmtnorec2lem  48017  2pwp1prm  48064  lighneallem2  48081  lighneallem3  48082  proththd  48089  ppivalnnprm  48100  ppivalnnnprmge6  48101  nn0o1gt2ALTV  48182  evenltle  48205  sbgoldbwt  48265  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  clnbgrval  48310  dfvopnbgr2  48341  uhgrimedgi  48378  gricushgr  48405  clnbgrgrim  48422  grimedg  48423  cycl3grtri  48435  isubgr3stgrlem4  48457  uspgrlimlem1  48476  grlimgrtri  48491  gpgedg2ov  48554  gpgedg2iv  48555  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  uspgropssxp  48632  lmod0rng  48717  lidldomn1  48719  zlidlring  48722  rngcinvALTV  48764  ztprmneprm  48835  lincext3  48944  zlmodzxznm  48985  suppdm  48998  elfzolborelfzop1  49007  nn0sumshdiglemB  49108  itcovalsucov  49156  lines  49219  rrx2vlinest  49229  line2xlem  49241  itschlc0yqe  49248  itsclquadeu  49265