Theorem eqcoms 2237

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2216

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

This theorem is referenced by:  gencbvex  2863  gencbval  2865  sbceq2a  3056  eqimss2  3297  uneqdifeqim  3599  tppreq3  3799  ifpprsnssdc  3804  copsex2t  4366  copsex2g  4367  ordsoexmid  4689  0elsucexmid  4692  ordpwsucexmid  4697  cnveqb  5223  cnveq0  5224  relcoi1  5299  funtpg  5412  f0rn0  5567  fimadmfo  5604  f1ssf1  5651  f1ocnvfv  5958  f1ocnvfvb  5959  cbvfo  5964  cbvexfo  5965  riotaeqimp  6036  brabvv  6107  ov6g  6200  ectocld  6848  ecoptocl  6869  phplem3  7121  f1dmvrnfibi  7224  f1vrnfibi  7225  updjud  7386  pr2ne  7502  nn0ind-raph  9716  nn01to3  9970  modqmuladd  10755  modqmuladdnn0  10757  fihashf1rn  11179  hashfzp1  11217  lswlgt0cl  11305  wrd2ind  11443  pfxccatin12lem2  11451  pfxccatin12lem3  11452  rennim  11715  xrmaxiflemcom  11962  m1expe  12613  m1expo  12614  m1exp1  12615  nn0o1gt2  12619  flodddiv4  12650  cncongr1  12828  m1dvdsndvds  12974  mgmsscl  13627  mndinvmod  13709  ringinvnzdiv  14296  txcn  15269  relogbcxpbap  15959  logbgcd1irr  15961  logbgcd1irraplemexp  15962  fsumdvdsmul  15988  zabsle1  16001  2lgslem1c  16092  2lgsoddprmlem3  16113  upgrpredgv  16270  usgredg2vlem2  16347  ushgredgedg  16350  ushgredgedgloop  16352  ifpsnprss  16467  upgrwlkvtxedg  16488  uspgr2wlkeq  16489  eupth2lem3lem3fi  16594  eupth2lem3lem4fi  16597  bj-inf2vnlem2  16880