Theorem eqcoms 2241

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3613  tppreq3  3814  ifpprsnssdc  3820  copsex2t  4385  copsex2g  4386  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  cnveqb  5243  cnveq0  5244  relcoi1  5319  funtpg  5432  f0rn0  5587  fimadmfo  5624  f1ssf1  5671  f1ocnvfv  5985  f1ocnvfvb  5986  cbvfo  5991  cbvexfo  5992  riotaeqimp  6063  brabvv  6134  ov6g  6227  ectocld  6875  ecoptocl  6896  phplem3  7155  f1dmvrnfibi  7258  f1vrnfibi  7259  updjud  7423  pr2ne  7539  nn0ind-raph  9768  nn01to3  10027  modqmuladd  10818  modqmuladdnn0  10820  fihashf1rn  11243  hashfzp1  11281  lswlgt0cl  11373  wrd2ind  11511  pfxccatin12lem2  11519  pfxccatin12lem3  11520  rennim  11784  xrmaxiflemcom  12034  m1expe  12685  m1expo  12686  m1exp1  12687  nn0o1gt2  12691  flodddiv4  12722  cncongr1  12900  m1dvdsndvds  13050  mgmsscl  13734  mndinvmod  13811  ringinvnzdiv  14439  txcn  15467  relogbcxpbap  16167  logbgcd1irr  16169  logbgcd1irraplemexp  16170  fsumdvdsmul  16251  zabsle1  16289  2lgslem1c  16380  2lgsoddprmlem3  16401  upgrpredgv  16558  usgredg2vlem2  16635  ushgredgedg  16638  ushgredgedgloop  16640  ifpsnprss  16755  upgrwlkvtxedg  16776  uspgr2wlkeq  16777  eupth2lem3lem3fi  16882  eupth2lem3lem4fi  16885  bj-inf2vnlem2  17168