Theorem eqcoms 2768

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 2767	. 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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  gencbvex  3506  sbceq2a  3750  eqimss2  3967  uneqdifeq  4447  tppreq3  4716  ifpprsnss  4721  tpprceq3  4763  preqsnd  4813  prproe  4832  copsex2t  5463  snopeqop  5477  opthhausdorff0  5490  optocl  5744  relopabi  5799  cnvimassrndmOLD  6199  unixpid  6287  reuop  6296  f0rn0  6767  fimadmfo  6805  f1ssf1  6857  tz6.12i  6911  fveqdmss  7078  fvcofneq  7093  funopsnOLD  7152  f1ocnvfv  7286  f1ocnvfvb  7287  cbvfo  7297  riotaeqimp  7403  ov6g  7584  tfindsg  7872  findsg  7909  mptcnfimad  7998  suppimacnv  8194  ectocld  8806  ecoptocl  8831  undifixp  8965  f1dmvrnfibi  9333  f1vrnfibi  9334  updjud  10018  card1  10052  prdom2  10088  sornom  10358  indpi  10995  ltlen  11414  eqlei  11423  squeeze0  12223  nn0ind-raph  12802  fzoopth  13900  injresinjlem  13928  fvf1tp  13932  modmuladd  14059  modmuladdnn0  14061  hashf1rn  14499  hashrabsn1  14521  hash1snb  14567  hashgt12el  14570  hashgt12el2  14571  hashfzp1  14579  hash2prde  14618  hash2pwpr  14624  fi1uzind  14655  brfi1indALT  14658  lswlgt0cl  14717  wrd2ind  14876  pfxccatin12lem2  14884  pfxccatin12lem3  14885  cshweqrep  14976  scshwfzeqfzo  14981  cshimadifsn  14984  cshimadifsn0  14985  2swrd2eqwrdeq  15111  wwlktovfo  15116  sgn3da  15259  rennim  15411  absmod0  15475  modfsummods  15965  mod2eq1n2dvds  16522  m1expe  16549  m1expo  16550  m1exp1  16551  nn0o1gt2  16556  flodddiv4  16590  cncongr1  16847  ge2nprmge4  16882  m1dvdsndvds  16981  cshwrepswhash1  17285  initoeu2lem1  18194  istos  18595  mgmsscl  18826  0gisid  18853  mndinvmod  18963  smndex1n0mnd  19116  symgfvne  19600  symgfix2  19635  symgextf1  19640  symgfixelsi  19654  psgnsn  19739  odbezout  19777  cntzcmnss  20060  frgpnabllem1  20092  ringinvnzdiv  20537  rngcinv  20894  psgndiflemB  21911  uvcendim  22158  selvvvval  22456  mamufacex  22716  smatvscl  22844  mavmulsolcl  22871  mdetunilem8  22939  pm2mpfo  23137  chpscmat  23165  chmaidscmat  23171  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  txcn  23950  qtopeu  24040  reeff1o  26779  relogbcxpb  27120  logbgcd1irr  27127  fsumdvdsmul  27527  zabsle1  27628  2lgslem1c  27725  2lgsoddprmlem3  27746  2sq2  27765  2sqreultlem  27779  2sqreunnltlem  27782  2sqreulem3  27785  pntrlog2bndlem5  27913  ltlesnd  28137  upgrpredgv  29722  usgredg2vlem2  29812  ushgredgedg  29815  ushgredgedgloop  29817  uhgrspan1  29889  nb3grprlem1  29966  uvtxnbgrb  29987  cusgrsize2inds  30039  1egrvtxdg0  30097  uspgrloopvtxel  30102  finsumvtxdg2size  30136  rusgrpropnb  30169  ifpsnprss  30208  upgrwlkvtxedg  30230  uspgr2wlkeq  30231  wlkp1lem5  30261  wlkp1  30265  usgr2pth  30355  spthcycl  30397  uspgrn2crct  30402  iswwlksnon  30447  wlkiswwlks1  30461  wlkiswwlks2lem3  30465  wwlksnextbi  30488  wwlksnredwwlkn0  30490  wwlksnextwrd  30491  wwlksnextsurj  30494  wwlksnextprop  30506  wspn0  30518  umgr2adedgwlkonALT  30541  umgr2adedgspth  30542  umgr2wlkon  30544  elwwlks2ons3  30549  elwwlks2on  30555  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  clwlkclwwlkf1lem3  30602  clwwlkfo  30646  eleclclwwlknlem2  30657  erclwwlkntr  30667  hashecclwwlkn1  30673  umgrhashecclwwlk  30674  0wlkonlem1  30714  upgr1wlkdlem1  30741  1pthon2v  30759  upgr3v3e3cycl  30786  uhgr3cyclexlem  30787  upgr4cycl4dv4e  30791  eupth2lem3lem3  30836  eupth2lem3lem4  30837  1to2vfriswmgr  30885  frgrncvvdeqlem6  30910  frgrncvvdeqlem8  30912  frgrncvvdeqlem9  30913  frgrwopreglem2  30919  2clwwlk2clwwlk  30956  extwwlkfab  30958  numclwwlk1lem2f1  30963  numclwwlkovh  30979  numclwwlk2lem1  30982  numclwlk2lem2f  30983  cdj1i  33040  brabgaf  33247  br8d  33249  kardcard2b  35889  onvf1odlem1  35950  onprcf1acwevdlem2  35965  goalrlem  36247  goalr  36248  fmlasucdisj  36250  satffunlem  36252  satffunlem1lem1  36253  satffunlem1lem2  36254  satffunlem2lem1  36255  satffunlem2lem2  36257  mthmb  36432  br8  36613  br4  36615  bj-snsetex  37968  bj-snglc  37974  copsex2d  38153  wl-dfcleq  38530  poimirlem20  38651  poimirlem26  38657  poimirlem27  38658  mblfinlem3  38670  mblfinlem4  38671  itg2addnclem  38682  indexdom  38761  ismgmOLD  38877  rngodm1dm2  38959  rngomndo  38962  rngoueqz  38967  zerdivemp1x  38974  opcon3b  40346  ps-1  40627  3atlem5  40637  4atex  41226  prjspvs  43731  iscard4  44627  pr2cv  44642  pm13.192  45487  iotavalsb  45510  relpfrlem  46036  fourierdlem32  47242  fourierdlem49  47258  fourierdlem64  47273  elprneb  48192  fveqvfvv  48203  funressnfv  48206  f1cof1b  48240  nvelim  48286  afvpcfv0  48309  afv0nbfvbi  48314  fnbrafvb  48317  tz6.12-afv  48336  afvco2  48339  ndmaovg  48347  afv2orxorb  48391  tz6.12-afv2  48403  tz6.12i-afv2  48406  f1oresf1o2  48454  nnmul2  48493  elsetpreimafvbi  48566  imasetpreimafvbijlemfo  48580  iccpartiltu  48597  fargshiftfv  48614  fargshiftf  48615  lswn0  48619  prsprel  48662  reupr  48697  2exopprim  48700  fmtnorec2lem  48720  2pwp1prm  48767  lighneallem2  48784  lighneallem3  48785  proththd  48792  ppivalnnprm  48803  ppivalnnnprmge6  48804  nn0o1gt2ALTV  48885  evenltle  48908  sbgoldbwt  48968  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  clnbgrval  49013  dfvopnbgr2  49044  uhgrimedgi  49081  gricushgr  49108  clnbgrgrim  49125  grimedg  49126  cycl3grtri  49138  isubgr3stgrlem4  49160  uspgrlimlem1  49179  grlimgrtri  49194  gpgedg2ov  49257  gpgedg2iv  49258  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem2lem3  49307  pgnbgreunbgrlem2  49308  pgnbgreunbgrlem4  49310  uspgropssxp  49335  lmod0rng  49419  lidldomn1  49421  zlidlring  49424  rngcinvALTV  49466  ztprmneprm  49552  lincext3  49661  zlmodzxznm  49702  suppdm  49715  elfzolborelfzop1  49724  nn0sumshdiglemB  49825  itcovalsucov  49873  lines  49937  rrx2vlinest  49946  line2xlem  49958  itschlc0yqe  49965  itsclquadeu  49982