Theorem eqcoms 2771

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

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  gencbvex  3511  sbceq2a  3757  eqimss2  3997  uneqdifeq  4454  tppreq3  4726  ifpprsnss  4731  tpprceq3  4773  preqsnd  4825  prproe  4871  copsex2t  5477  snopeqop  5491  opthhausdorff0  5503  optocl  5757  relopabi  5811  cnvimassrndm  6151  cnveqb  6197  cnveq0  6198  unixpid  6287  reuop  6296  f0rn0  6765  fimadmfo  6803  f1ssf1  6855  tz6.12i  6909  fveqdmss  7075  fvcofneq  7090  funopsnOLD  7147  f1ocnvfv  7278  f1ocnvfvb  7279  cbvfo  7289  riotaeqimp  7395  ov6g  7576  tfindsg  7858  findsg  7895  mptcnfimad  7984  suppimacnv  8171  ectocld  8781  ecoptocl  8806  undifixp  8933  f1dmvrnfibi  9299  f1vrnfibi  9300  updjud  9921  card1  9955  prdom2  9991  sornom  10262  indpi  10893  ltlen  11312  eqlei  11321  squeeze0  12119  nn0ind-raph  12697  fzoopth  13793  injresinjlem  13821  fvf1tp  13824  modmuladd  13951  modmuladdnn0  13953  hashf1rn  14390  hashrabsn1  14412  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hashfzp1  14470  hash2prde  14509  hash2pwpr  14515  fi1uzind  14546  brfi1indALT  14549  lswlgt0cl  14608  wrd2ind  14762  pfxccatin12lem2  14770  pfxccatin12lem3  14771  cshweqrep  14860  scshwfzeqfzo  14865  cshimadifsn  14868  cshimadifsn0  14869  2swrd2eqwrdeq  14992  wwlktovfo  14997  sgn3da  15140  rennim  15292  absmod0  15356  modfsummods  15847  mod2eq1n2dvds  16406  m1expe  16433  m1expo  16434  m1exp1  16435  nn0o1gt2  16440  flodddiv4  16474  cncongr1  16726  ge2nprmge4  16761  m1dvdsndvds  16859  cshwrepswhash1  17163  initoeu2lem1  18072  istos  18473  mgmsscl  18704  mndinvmod  18823  smndex1n0mnd  18975  symgfvne  19452  symgfix2  19487  symgextf1  19492  symgfixelsi  19506  psgnsn  19591  odbezout  19629  cntzcmnss  19912  frgpnabllem1  19944  ringinvnzdiv  20385  rngcinv  20723  psgndiflemB  21731  uvcendim  21978  selvvvval  22274  mamufacex  22534  smatvscl  22662  mavmulsolcl  22689  mdetunilem8  22757  pm2mpfo  22952  chpscmat  22980  chmaidscmat  22986  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  txcn  23764  qtopeu  23854  reeff1o  26588  relogbcxpb  26930  logbgcd1irr  26937  fsumdvdsmul  27337  zabsle1  27438  2lgslem1c  27535  2lgsoddprmlem3  27556  2sq2  27575  2sqreultlem  27589  2sqreunnltlem  27592  2sqreulem3  27595  pntrlog2bndlem5  27723  ltlesnd  27917  upgrpredgv  29467  usgredg2vlem2  29554  ushgredgedg  29557  ushgredgedgloop  29559  uhgrspan1  29631  nb3grprlem1  29708  uvtxnbgrb  29729  cusgrsize2inds  29781  1egrvtxdg0  29839  uspgrloopvtxel  29844  finsumvtxdg2size  29878  rusgrpropnb  29911  ifpsnprss  29950  upgrwlkvtxedg  29972  uspgr2wlkeq  29973  wlkp1lem5  30003  wlkp1  30007  usgr2pth  30091  uspgrn2crct  30135  iswwlksnon  30180  wlkiswwlks1  30194  wlkiswwlks2lem3  30198  wwlksnextbi  30221  wwlksnredwwlkn0  30223  wwlksnextwrd  30224  wwlksnextsurj  30227  wwlksnextprop  30239  wspn0  30251  umgr2adedgwlkonALT  30274  umgr2adedgspth  30275  umgr2wlkon  30277  elwwlks2ons3  30282  elwwlks2on  30288  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  clwlkclwwlkf1lem3  30335  clwwlkfo  30379  eleclclwwlknlem2  30390  erclwwlkntr  30400  hashecclwwlkn1  30406  umgrhashecclwwlk  30407  0wlkonlem1  30447  upgr1wlkdlem1  30474  1pthon2v  30482  upgr3v3e3cycl  30509  uhgr3cyclexlem  30510  upgr4cycl4dv4e  30514  eupth2lem3lem3  30559  eupth2lem3lem4  30560  1to2vfriswmgr  30608  frgrncvvdeqlem6  30633  frgrncvvdeqlem8  30635  frgrncvvdeqlem9  30636  frgrwopreglem2  30642  2clwwlk2clwwlk  30679  extwwlkfab  30681  numclwwlk1lem2f1  30686  numclwwlkovh  30702  numclwwlk2lem1  30705  numclwlk2lem2f  30706  cdj1i  32763  brabgaf  32929  br8d  32931  kardcard2b  35556  onvf1odlem1  35565  spthcycl  35599  goalrlem  35866  goalr  35867  fmlasucdisj  35869  satffunlem  35871  satffunlem1lem1  35872  satffunlem1lem2  35873  satffunlem2lem1  35874  satffunlem2lem2  35876  mthmb  36051  br8  36226  br4  36228  bj-snsetex  37577  bj-snglc  37583  copsex2d  37761  wl-dfcleq  38138  poimirlem20  38269  poimirlem26  38275  poimirlem27  38276  mblfinlem3  38288  mblfinlem4  38289  itg2addnclem  38300  indexdom  38363  ismgmOLD  38479  rngodm1dm2  38561  rngomndo  38564  rngoueqz  38569  zerdivemp1x  38576  opcon3b  39948  ps-1  40229  3atlem5  40239  4atex  40828  prjspvs  43322  iscard4  44239  pr2cv  44254  pm13.192  45100  iotavalsb  45123  relpfrlem  45642  fourierdlem32  46833  fourierdlem49  46849  fourierdlem64  46864  elprneb  47743  fveqvfvv  47754  funressnfv  47757  f1cof1b  47791  nvelim  47837  afvpcfv0  47860  afv0nbfvbi  47865  fnbrafvb  47868  tz6.12-afv  47887  afvco2  47890  ndmaovg  47898  afv2orxorb  47942  tz6.12-afv2  47954  tz6.12i-afv2  47957  f1oresf1o2  48005  nnmul2  48044  elsetpreimafvbi  48117  imasetpreimafvbijlemfo  48131  iccpartiltu  48148  fargshiftfv  48165  fargshiftf  48166  lswn0  48170  prsprel  48213  reupr  48248  2exopprim  48251  fmtnorec2lem  48271  2pwp1prm  48318  lighneallem2  48335  lighneallem3  48336  proththd  48343  ppivalnnprm  48354  ppivalnnnprmge6  48355  nn0o1gt2ALTV  48436  evenltle  48459  sbgoldbwt  48519  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  clnbgrval  48564  dfvopnbgr2  48595  uhgrimedgi  48632  gricushgr  48659  clnbgrgrim  48676  grimedg  48677  cycl3grtri  48689  isubgr3stgrlem4  48711  uspgrlimlem1  48730  grlimgrtri  48745  gpgedg2ov  48808  gpgedg2iv  48809  pgnbgreunbgrlem1  48855  pgnbgreunbgrlem2lem3  48858  pgnbgreunbgrlem2  48859  pgnbgreunbgrlem4  48861  uspgropssxp  48886  lmod0rng  48971  lidldomn1  48973  zlidlring  48976  rngcinvALTV  49018  ztprmneprm  49104  lincext3  49213  zlmodzxznm  49254  suppdm  49267  elfzolborelfzop1  49276  nn0sumshdiglemB  49377  itcovalsucov  49425  lines  49488  rrx2vlinest  49498  line2xlem  49510  itschlc0yqe  49517  itsclquadeu  49534