Theorem eqcoms 2806

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

Syntax hints:   → wi 4   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  gencbvex  3497  sbceq2a  3732  eqimss2  3972  uneqdifeq  4396  tppreq3  4655  ifpprsnss  4660  tpprceq3  4697  preqsnd  4749  elpr2elpr  4759  prproe  4798  copsex2t  5348  copsex2g  5349  snopeqop  5361  opthhausdorff0  5373  relopabi  5658  cnveqb  6020  cnveq0  6021  unixpid  6103  reuop  6112  f0rn0  6538  fimadmfo  6574  f1ssf1  6621  tz6.12i  6671  fveqdmss  6823  fvcofneq  6836  funopsn  6887  f1ocnvfv  7013  f1ocnvfvb  7014  cbvfo  7023  riotaeqimp  7119  ov6g  7292  tfindsg  7555  findsg  7590  suppimacnv  7824  suppss  7843  ectocld  8347  ecoptocl  8370  undifixp  8481  phplem3  8682  f1dmvrnfibi  8792  f1vrnfibi  8793  updjud  9347  card1  9381  pr2ne  9416  prdom2  9417  sornom  9688  indpi  10318  ltlen  10730  eqlei  10739  squeeze0  11532  nn0ind-raph  12070  injresinjlem  13152  modmuladd  13276  modmuladdnn0  13278  hashf1rn  13709  hashrabsn1  13731  hash1snb  13776  hashgt12el  13779  hashgt12el2  13780  hashfzp1  13788  hash2prde  13824  hash2pwpr  13830  fi1uzind  13851  brfi1indALT  13854  lswlgt0cl  13912  wrd2ind  14076  pfxccatin12lem2  14084  pfxccatin12lem3  14085  cshweqrep  14174  cshwsexa  14177  scshwfzeqfzo  14179  cshimadifsn  14182  cshimadifsn0  14183  2swrd2eqwrdeq  14306  wwlktovfo  14313  rennim  14590  absmod0  14655  modfsummods  15140  mod2eq1n2dvds  15688  m1expe  15715  m1expo  15716  m1exp1  15717  nn0o1gt2  15722  flodddiv4  15754  cncongr1  16001  ge2nprmge4  16035  m1dvdsndvds  16125  cshwrepswhash1  16428  initoeu2lem1  17266  istos  17637  mgmsscl  17849  mndinvmod  17933  smndex1n0mnd  18069  symgfvne  18501  symgfix2  18536  symgextf1  18541  symgfixelsi  18555  psgnsn  18640  odbezout  18677  cntzcmnss  18954  frgpnabllem1  18986  ringinvnzdiv  19339  psgndiflemB  20289  uvcendim  20536  mamufacex  20996  smatvscl  21129  mavmulsolcl  21156  mdetunilem8  21224  pm2mpfo  21419  chpscmat  21447  chmaidscmat  21453  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  txcn  22231  qtopeu  22321  reeff1o  25042  relogbcxpb  25373  logbgcd1irr  25380  zabsle1  25880  2lgslem1c  25977  2lgsoddprmlem3  25998  2sq2  26017  2sqreultlem  26031  2sqreunnltlem  26034  2sqreulem3  26037  pntrlog2bndlem5  26165  upgrpredgv  26932  usgredg2vlem2  27016  ushgredgedg  27019  ushgredgedgloop  27021  uhgrspan1  27093  nb3grprlem1  27170  uvtxnbgrb  27191  cusgrsize2inds  27243  1egrvtxdg0  27301  uspgrloopvtxel  27306  finsumvtxdg2size  27340  rusgrpropnb  27373  ifpsnprss  27412  upgrwlkvtxedg  27434  uspgr2wlkeq  27435  wlkp1lem5  27467  wlkp1  27471  usgr2pth  27553  uspgrn2crct  27594  iswwlksnon  27639  wlkiswwlks1  27653  wlkiswwlks2lem3  27657  wwlksnextbi  27680  wwlksnredwwlkn0  27682  wwlksnextwrd  27683  wwlksnextsurj  27686  wwlksnextprop  27698  wspn0  27710  umgr2adedgwlkonALT  27733  umgr2adedgspth  27734  umgr2wlkon  27736  elwwlks2ons3  27741  elwwlks2on  27745  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlkf1lem3  27791  clwwlkfo  27835  eleclclwwlknlem2  27846  erclwwlkntr  27856  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  0wlkonlem1  27903  upgr1wlkdlem1  27930  1pthon2v  27938  upgr3v3e3cycl  27965  uhgr3cyclexlem  27966  upgr4cycl4dv4e  27970  eupth2lem3lem3  28015  eupth2lem3lem4  28016  1to2vfriswmgr  28064  frgrncvvdeqlem6  28089  frgrncvvdeqlem8  28091  frgrncvvdeqlem9  28092  frgrwopreglem2  28098  2clwwlk2clwwlk  28135  extwwlkfab  28137  numclwwlk1lem2f1  28142  numclwwlkovh  28158  numclwwlk2lem1  28161  numclwlk2lem2f  28162  cdj1i  30216  brabgaf  30372  br8d  30374  sgn3da  31909  spthcycl  32489  goalrlem  32756  goalr  32757  fmlasucdisj  32759  satffunlem  32761  satffunlem1lem1  32762  satffunlem1lem2  32763  satffunlem2lem1  32764  satffunlem2lem2  32766  mthmb  32941  br8  33105  br4  33107  bj-snsetex  34399  bj-snglc  34405  copsex2d  34554  poimirlem20  35077  poimirlem26  35083  poimirlem27  35084  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  indexdom  35172  ismgmOLD  35288  rngodm1dm2  35370  rngomndo  35373  rngoueqz  35378  zerdivemp1x  35385  opcon3b  36492  ps-1  36773  3atlem5  36783  4atex  37372  prjspvs  39604  iscard4  40241  pr2cv  40247  pm13.192  41114  iotavalsb  41137  fourierdlem32  42781  fourierdlem49  42797  fourierdlem64  42812  elprneb  43621  fveqvfvv  43632  funressnfv  43635  nvelim  43679  afvpcfv0  43702  afv0nbfvbi  43707  fnbrafvb  43710  tz6.12-afv  43729  afvco2  43732  ndmaovg  43740  afv2orxorb  43784  tz6.12-afv2  43796  tz6.12i-afv2  43799  f1oresf1o2  43847  fzoopth  43884  elsetpreimafvbi  43908  imasetpreimafvbijlemfo  43922  iccpartiltu  43939  fargshiftfv  43956  fargshiftf  43957  lswn0  43961  prsprel  44004  reupr  44039  2exopprim  44042  fmtnorec2lem  44059  2pwp1prm  44106  lighneallem2  44124  lighneallem3  44125  proththd  44132  nn0o1gt2ALTV  44212  evenltle  44235  sbgoldbwt  44295  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  isomushgr  44344  isomuspgrlem1  44345  uspgropssxp  44372  lmod0rng  44492  lidldomn1  44545  zlidlring  44552  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  ztprmneprm  44749  lincext3  44865  zlmodzxznm  44906  suppdm  44919  elfzolborelfzop1  44928  nn0sumshdiglemB  45034  itcovalsucov  45082  lines  45145  rrx2vlinest  45155  line2xlem  45167  itschlc0yqe  45174  itsclquadeu  45191