Theorem eqcoms 2235

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  gencbvex  2860  gencbval  2862  sbceq2a  3052  eqimss2  3292  uneqdifeqim  3594  tppreq3  3793  ifpprsnssdc  3798  copsex2t  4360  copsex2g  4361  ordsoexmid  4683  0elsucexmid  4686  ordpwsucexmid  4691  cnveqb  5217  cnveq0  5218  relcoi1  5293  funtpg  5406  f0rn0  5561  fimadmfo  5598  f1ssf1  5645  f1ocnvfv  5951  f1ocnvfvb  5952  cbvfo  5957  cbvexfo  5958  riotaeqimp  6027  brabvv  6098  ov6g  6191  ectocld  6834  ecoptocl  6855  phplem3  7107  f1dmvrnfibi  7210  f1vrnfibi  7211  updjud  7372  pr2ne  7488  nn0ind-raph  9691  nn01to3  9945  modqmuladd  10724  modqmuladdnn0  10726  fihashf1rn  11146  hashfzp1  11184  lswlgt0cl  11270  wrd2ind  11408  pfxccatin12lem2  11416  pfxccatin12lem3  11417  rennim  11680  xrmaxiflemcom  11927  m1expe  12578  m1expo  12579  m1exp1  12580  nn0o1gt2  12584  flodddiv4  12615  cncongr1  12793  m1dvdsndvds  12939  mgmsscl  13563  mndinvmod  13647  ringinvnzdiv  14183  txcn  15127  relogbcxpbap  15817  logbgcd1irr  15819  logbgcd1irraplemexp  15820  fsumdvdsmul  15846  zabsle1  15859  2lgslem1c  15950  2lgsoddprmlem3  15971  upgrpredgv  16128  usgredg2vlem2  16205  ushgredgedg  16208  ushgredgedgloop  16210  ifpsnprss  16325  upgrwlkvtxedg  16346  uspgr2wlkeq  16347  eupth2lem3lem3fi  16452  eupth2lem3lem4fi  16455  bj-inf2vnlem2  16728