Theorem eqcoms 2232

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcoms.1	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
eqcoms	⊢ (𝐵 = 𝐴 → 𝜑)

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2231	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 121	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  gencbvex  2847  gencbval  2849  sbceq2a  3039  eqimss2  3279  uneqdifeqim  3577  tppreq3  3769  ifpprsnssdc  3774  copsex2t  4332  copsex2g  4333  ordsoexmid  4655  0elsucexmid  4658  ordpwsucexmid  4663  cnveqb  5187  cnveq0  5188  relcoi1  5263  funtpg  5375  f0rn0  5525  fimadmfo  5562  f1ocnvfv  5912  f1ocnvfvb  5913  cbvfo  5918  cbvexfo  5919  riotaeqimp  5988  brabvv  6059  ov6g  6152  ectocld  6761  ecoptocl  6782  phplem3  7028  f1dmvrnfibi  7127  f1vrnfibi  7128  updjud  7265  pr2ne  7381  nn0ind-raph  9580  nn01to3  9829  modqmuladd  10605  modqmuladdnn0  10607  fihashf1rn  11027  hashfzp1  11064  lswlgt0cl  11142  wrd2ind  11276  pfxccatin12lem2  11284  pfxccatin12lem3  11285  rennim  11534  xrmaxiflemcom  11781  m1expe  12431  m1expo  12432  m1exp1  12433  nn0o1gt2  12437  flodddiv4  12468  cncongr1  12646  m1dvdsndvds  12792  mgmsscl  13415  mndinvmod  13499  ringinvnzdiv  14034  txcn  14970  relogbcxpbap  15660  logbgcd1irr  15662  logbgcd1irraplemexp  15663  fsumdvdsmul  15686  zabsle1  15699  2lgslem1c  15790  2lgsoddprmlem3  15811  upgrpredgv  15965  usgredg2vlem2  16042  ushgredgedg  16045  ushgredgedgloop  16047  ifpsnprss  16115  upgrwlkvtxedg  16136  uspgr2wlkeq  16137  bj-inf2vnlem2  16443