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  2848  gencbval  2850  sbceq2a  3040  eqimss2  3280  uneqdifeqim  3578  tppreq3  3772  ifpprsnssdc  3777  copsex2t  4335  copsex2g  4336  ordsoexmid  4658  0elsucexmid  4661  ordpwsucexmid  4666  cnveqb  5190  cnveq0  5191  relcoi1  5266  funtpg  5378  f0rn0  5528  fimadmfo  5565  f1ocnvfv  5915  f1ocnvfvb  5916  cbvfo  5921  cbvexfo  5922  riotaeqimp  5991  brabvv  6062  ov6g  6155  ectocld  6765  ecoptocl  6786  phplem3  7035  f1dmvrnfibi  7137  f1vrnfibi  7138  updjud  7275  pr2ne  7391  nn0ind-raph  9590  nn01to3  9844  modqmuladd  10621  modqmuladdnn0  10623  fihashf1rn  11043  hashfzp1  11081  lswlgt0cl  11159  wrd2ind  11297  pfxccatin12lem2  11305  pfxccatin12lem3  11306  rennim  11556  xrmaxiflemcom  11803  m1expe  12453  m1expo  12454  m1exp1  12455  nn0o1gt2  12459  flodddiv4  12490  cncongr1  12668  m1dvdsndvds  12814  mgmsscl  13437  mndinvmod  13521  ringinvnzdiv  14056  txcn  14992  relogbcxpbap  15682  logbgcd1irr  15684  logbgcd1irraplemexp  15685  fsumdvdsmul  15708  zabsle1  15721  2lgslem1c  15812  2lgsoddprmlem3  15833  upgrpredgv  15990  usgredg2vlem2  16067  ushgredgedg  16070  ushgredgedgloop  16072  ifpsnprss  16154  upgrwlkvtxedg  16175  uspgr2wlkeq  16176  bj-inf2vnlem2  16516