Theorem eqcoms 2234

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 2233	. 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 2213

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

This theorem is referenced by:  gencbvex  2850  gencbval  2852  sbceq2a  3042  eqimss2  3282  uneqdifeqim  3580  tppreq3  3774  ifpprsnssdc  3779  copsex2t  4337  copsex2g  4338  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  cnveqb  5192  cnveq0  5193  relcoi1  5268  funtpg  5381  f0rn0  5531  fimadmfo  5568  f1ssf1  5615  f1ocnvfv  5920  f1ocnvfvb  5921  cbvfo  5926  cbvexfo  5927  riotaeqimp  5996  brabvv  6067  ov6g  6160  ectocld  6770  ecoptocl  6791  phplem3  7040  f1dmvrnfibi  7143  f1vrnfibi  7144  updjud  7281  pr2ne  7397  nn0ind-raph  9597  nn01to3  9851  modqmuladd  10629  modqmuladdnn0  10631  fihashf1rn  11051  hashfzp1  11089  lswlgt0cl  11167  wrd2ind  11305  pfxccatin12lem2  11313  pfxccatin12lem3  11314  rennim  11564  xrmaxiflemcom  11811  m1expe  12462  m1expo  12463  m1exp1  12464  nn0o1gt2  12468  flodddiv4  12499  cncongr1  12677  m1dvdsndvds  12823  mgmsscl  13446  mndinvmod  13530  ringinvnzdiv  14066  txcn  15002  relogbcxpbap  15692  logbgcd1irr  15694  logbgcd1irraplemexp  15695  fsumdvdsmul  15718  zabsle1  15731  2lgslem1c  15822  2lgsoddprmlem3  15843  upgrpredgv  16000  usgredg2vlem2  16077  ushgredgedg  16080  ushgredgedgloop  16082  ifpsnprss  16197  upgrwlkvtxedg  16218  uspgr2wlkeq  16219  eupth2lem3lem3fi  16324  eupth2lem3lem4fi  16327  bj-inf2vnlem2  16587