Theorem eqcoms 2233

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-ext 2212

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

This theorem is referenced by:  gencbvex  2849  gencbval  2851  sbceq2a  3041  eqimss2  3281  uneqdifeqim  3579  tppreq3  3775  ifpprsnssdc  3780  copsex2t  4339  copsex2g  4340  ordsoexmid  4662  0elsucexmid  4665  ordpwsucexmid  4670  cnveqb  5194  cnveq0  5195  relcoi1  5270  funtpg  5383  f0rn0  5534  fimadmfo  5571  f1ssf1  5618  f1ocnvfv  5925  f1ocnvfvb  5926  cbvfo  5931  cbvexfo  5932  riotaeqimp  6001  brabvv  6072  ov6g  6165  ectocld  6775  ecoptocl  6796  phplem3  7045  f1dmvrnfibi  7148  f1vrnfibi  7149  updjud  7286  pr2ne  7402  nn0ind-raph  9602  nn01to3  9856  modqmuladd  10634  modqmuladdnn0  10636  fihashf1rn  11056  hashfzp1  11094  lswlgt0cl  11175  wrd2ind  11313  pfxccatin12lem2  11321  pfxccatin12lem3  11322  rennim  11585  xrmaxiflemcom  11832  m1expe  12483  m1expo  12484  m1exp1  12485  nn0o1gt2  12489  flodddiv4  12520  cncongr1  12698  m1dvdsndvds  12844  mgmsscl  13467  mndinvmod  13551  ringinvnzdiv  14087  txcn  15028  relogbcxpbap  15718  logbgcd1irr  15720  logbgcd1irraplemexp  15721  fsumdvdsmul  15744  zabsle1  15757  2lgslem1c  15848  2lgsoddprmlem3  15869  upgrpredgv  16026  usgredg2vlem2  16103  ushgredgedg  16106  ushgredgedgloop  16108  ifpsnprss  16223  upgrwlkvtxedg  16244  uspgr2wlkeq  16245  eupth2lem3lem3fi  16350  eupth2lem3lem4fi  16353  bj-inf2vnlem2  16626