Theorem eqcoms 2237

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 2236	. 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 2216

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

This theorem is referenced by:  gencbvex  2863  gencbval  2865  sbceq2a  3055  eqimss2  3295  uneqdifeqim  3597  tppreq3  3796  ifpprsnssdc  3801  copsex2t  4363  copsex2g  4364  ordsoexmid  4686  0elsucexmid  4689  ordpwsucexmid  4694  cnveqb  5220  cnveq0  5221  relcoi1  5296  funtpg  5409  f0rn0  5564  fimadmfo  5601  f1ssf1  5648  f1ocnvfv  5954  f1ocnvfvb  5955  cbvfo  5960  cbvexfo  5961  riotaeqimp  6030  brabvv  6101  ov6g  6194  ectocld  6837  ecoptocl  6858  phplem3  7110  f1dmvrnfibi  7213  f1vrnfibi  7214  updjud  7375  pr2ne  7491  nn0ind-raph  9701  nn01to3  9955  modqmuladd  10735  modqmuladdnn0  10737  fihashf1rn  11159  hashfzp1  11197  lswlgt0cl  11285  wrd2ind  11423  pfxccatin12lem2  11431  pfxccatin12lem3  11432  rennim  11695  xrmaxiflemcom  11942  m1expe  12593  m1expo  12594  m1exp1  12595  nn0o1gt2  12599  flodddiv4  12630  cncongr1  12808  m1dvdsndvds  12954  mgmsscl  13595  mndinvmod  13679  ringinvnzdiv  14215  txcn  15189  relogbcxpbap  15879  logbgcd1irr  15881  logbgcd1irraplemexp  15882  fsumdvdsmul  15908  zabsle1  15921  2lgslem1c  16012  2lgsoddprmlem3  16033  upgrpredgv  16190  usgredg2vlem2  16267  ushgredgedg  16270  ushgredgedgloop  16272  ifpsnprss  16387  upgrwlkvtxedg  16408  uspgr2wlkeq  16409  eupth2lem3lem3fi  16514  eupth2lem3lem4fi  16517  bj-inf2vnlem2  16790