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  7422  pr2ne  7538  nn0ind-raph  9765  nn01to3  10019  modqmuladd  10805  modqmuladdnn0  10807  fihashf1rn  11229  hashfzp1  11267  lswlgt0cl  11359  wrd2ind  11497  pfxccatin12lem2  11505  pfxccatin12lem3  11506  rennim  11770  xrmaxiflemcom  12017  m1expe  12668  m1expo  12669  m1exp1  12670  nn0o1gt2  12674  flodddiv4  12705  cncongr1  12883  m1dvdsndvds  13029  mgmsscl  13683  mndinvmod  13760  ringinvnzdiv  14357  txcn  15378  relogbcxpbap  16073  logbgcd1irr  16075  logbgcd1irraplemexp  16076  fsumdvdsmul  16111  zabsle1  16130  2lgslem1c  16221  2lgsoddprmlem3  16242  upgrpredgv  16399  usgredg2vlem2  16476  ushgredgedg  16479  ushgredgedgloop  16481  ifpsnprss  16596  upgrwlkvtxedg  16617  uspgr2wlkeq  16618  eupth2lem3lem3fi  16723  eupth2lem3lem4fi  16726  bj-inf2vnlem2  17009