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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  gencbvex  3509  sbceq2a  3754  eqimss2  3993  uneqdifeq  4451  tppreq3  4723  ifpprsnss  4728  tpprceq3  4770  preqsnd  4822  prproe  4868  copsex2t  5473  snopeqop  5487  opthhausdorff0  5499  optocl  5753  relopabi  5807  cnvimassrndm  6147  cnveqb  6194  cnveq0  6195  unixpid  6286  reuop  6295  f0rn0  6764  fimadmfo  6802  f1ssf1  6854  tz6.12i  6908  fveqdmss  7075  fvcofneq  7090  funopsnOLD  7149  f1ocnvfv  7283  f1ocnvfvb  7284  cbvfo  7294  riotaeqimp  7400  ov6g  7581  tfindsg  7861  findsg  7898  mptcnfimad  7987  suppimacnv  8176  ectocld  8786  ecoptocl  8811  undifixp  8945  f1dmvrnfibi  9312  f1vrnfibi  9313  updjud  9943  card1  9977  prdom2  10013  sornom  10283  indpi  10920  ltlen  11339  eqlei  11348  squeeze0  12146  nn0ind-raph  12725  fzoopth  13822  injresinjlem  13850  fvf1tp  13854  modmuladd  13981  modmuladdnn0  13983  hashf1rn  14420  hashrabsn1  14442  hash1snb  14488  hashgt12el  14491  hashgt12el2  14492  hashfzp1  14500  hash2prde  14539  hash2pwpr  14545  fi1uzind  14576  brfi1indALT  14579  lswlgt0cl  14638  wrd2ind  14796  pfxccatin12lem2  14804  pfxccatin12lem3  14805  cshweqrep  14896  scshwfzeqfzo  14901  cshimadifsn  14904  cshimadifsn0  14905  2swrd2eqwrdeq  15030  wwlktovfo  15035  sgn3da  15178  rennim  15330  absmod0  15394  modfsummods  15884  mod2eq1n2dvds  16443  m1expe  16470  m1expo  16471  m1exp1  16472  nn0o1gt2  16477  flodddiv4  16511  cncongr1  16763  ge2nprmge4  16798  m1dvdsndvds  16896  cshwrepswhash1  17200  initoeu2lem1  18109  istos  18510  mgmsscl  18741  0gisid  18767  mndinvmod  18877  smndex1n0mnd  19030  symgfvne  19514  symgfix2  19549  symgextf1  19554  symgfixelsi  19568  psgnsn  19653  odbezout  19691  cntzcmnss  19974  frgpnabllem1  20006  ringinvnzdiv  20449  rngcinv  20805  psgndiflemB  21819  uvcendim  22066  selvvvval  22364  mamufacex  22624  smatvscl  22752  mavmulsolcl  22779  mdetunilem8  22847  pm2mpfo  23045  chpscmat  23073  chmaidscmat  23079  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  txcn  23858  qtopeu  23948  reeff1o  26690  relogbcxpb  27032  logbgcd1irr  27039  fsumdvdsmul  27439  zabsle1  27540  2lgslem1c  27637  2lgsoddprmlem3  27658  2sq2  27677  2sqreultlem  27691  2sqreunnltlem  27694  2sqreulem3  27697  pntrlog2bndlem5  27825  ltlesnd  28019  upgrpredgv  29604  usgredg2vlem2  29694  ushgredgedg  29697  ushgredgedgloop  29699  uhgrspan1  29771  nb3grprlem1  29848  uvtxnbgrb  29869  cusgrsize2inds  29921  1egrvtxdg0  29979  uspgrloopvtxel  29984  finsumvtxdg2size  30018  rusgrpropnb  30051  ifpsnprss  30090  upgrwlkvtxedg  30112  uspgr2wlkeq  30113  wlkp1lem5  30143  wlkp1  30147  usgr2pth  30237  spthcycl  30279  uspgrn2crct  30284  iswwlksnon  30329  wlkiswwlks1  30343  wlkiswwlks2lem3  30347  wwlksnextbi  30370  wwlksnredwwlkn0  30372  wwlksnextwrd  30373  wwlksnextsurj  30376  wwlksnextprop  30388  wspn0  30400  umgr2adedgwlkonALT  30423  umgr2adedgspth  30424  umgr2wlkon  30426  elwwlks2ons3  30431  elwwlks2on  30437  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlkf1lem3  30484  clwwlkfo  30528  eleclclwwlknlem2  30539  erclwwlkntr  30549  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  0wlkonlem1  30596  upgr1wlkdlem1  30623  1pthon2v  30641  upgr3v3e3cycl  30668  uhgr3cyclexlem  30669  upgr4cycl4dv4e  30673  eupth2lem3lem3  30718  eupth2lem3lem4  30719  1to2vfriswmgr  30767  frgrncvvdeqlem6  30792  frgrncvvdeqlem8  30794  frgrncvvdeqlem9  30795  frgrwopreglem2  30801  2clwwlk2clwwlk  30838  extwwlkfab  30840  numclwwlk1lem2f1  30845  numclwwlkovh  30861  numclwwlk2lem1  30864  numclwlk2lem2f  30865  cdj1i  32922  brabgaf  33087  br8d  33089  kardcard2b  35699  onvf1odlem1  35708  goalrlem  35983  goalr  35984  fmlasucdisj  35986  satffunlem  35988  satffunlem1lem1  35989  satffunlem1lem2  35990  satffunlem2lem1  35991  satffunlem2lem2  35993  mthmb  36168  br8  36343  br4  36345  bj-snsetex  37715  bj-snglc  37721  copsex2d  37899  wl-dfcleq  38276  poimirlem20  38397  poimirlem26  38403  poimirlem27  38404  mblfinlem3  38416  mblfinlem4  38417  itg2addnclem  38428  indexdom  38492  ismgmOLD  38608  rngodm1dm2  38690  rngomndo  38693  rngoueqz  38698  zerdivemp1x  38705  opcon3b  40077  ps-1  40358  3atlem5  40368  4atex  40957  prjspvs  43464  iscard4  44381  pr2cv  44396  pm13.192  45242  iotavalsb  45265  relpfrlem  45784  fourierdlem32  46975  fourierdlem49  46991  fourierdlem64  47006  elprneb  47925  fveqvfvv  47936  funressnfv  47939  f1cof1b  47973  nvelim  48019  afvpcfv0  48042  afv0nbfvbi  48047  fnbrafvb  48050  tz6.12-afv  48069  afvco2  48072  ndmaovg  48080  afv2orxorb  48124  tz6.12-afv2  48136  tz6.12i-afv2  48139  f1oresf1o2  48187  nnmul2  48226  elsetpreimafvbi  48299  imasetpreimafvbijlemfo  48313  iccpartiltu  48330  fargshiftfv  48347  fargshiftf  48348  lswn0  48352  prsprel  48395  reupr  48430  2exopprim  48433  fmtnorec2lem  48453  2pwp1prm  48500  lighneallem2  48517  lighneallem3  48518  proththd  48525  ppivalnnprm  48536  ppivalnnnprmge6  48537  nn0o1gt2ALTV  48618  evenltle  48641  sbgoldbwt  48701  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  clnbgrval  48746  dfvopnbgr2  48777  uhgrimedgi  48814  gricushgr  48841  clnbgrgrim  48858  grimedg  48859  cycl3grtri  48871  isubgr3stgrlem4  48893  uspgrlimlem1  48912  grlimgrtri  48927  gpgedg2ov  48990  gpgedg2iv  48991  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem2  49041  pgnbgreunbgrlem4  49043  uspgropssxp  49068  lmod0rng  49152  lidldomn1  49154  zlidlring  49157  rngcinvALTV  49199  ztprmneprm  49285  lincext3  49394  zlmodzxznm  49435  suppdm  49448  elfzolborelfzop1  49457  nn0sumshdiglemB  49558  itcovalsucov  49606  lines  49669  rrx2vlinest  49679  line2xlem  49691  itschlc0yqe  49698  itsclquadeu  49715