Theorem eqcoms 2232

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  gencbvex  2847  gencbval  2849  sbceq2a  3039  eqimss2  3279  uneqdifeqim  3577  tppreq3  3769  ifpprsnssdc  3774  copsex2t  4331  copsex2g  4332  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  cnveqb  5184  cnveq0  5185  relcoi1  5260  funtpg  5372  f0rn0  5522  fimadmfo  5559  f1ocnvfv  5909  f1ocnvfvb  5910  cbvfo  5915  cbvexfo  5916  riotaeqimp  5985  brabvv  6056  ov6g  6149  ectocld  6756  ecoptocl  6777  phplem3  7023  f1dmvrnfibi  7119  f1vrnfibi  7120  updjud  7257  pr2ne  7373  nn0ind-raph  9572  nn01to3  9820  modqmuladd  10596  modqmuladdnn0  10598  fihashf1rn  11018  hashfzp1  11054  lswlgt0cl  11132  wrd2ind  11263  pfxccatin12lem2  11271  pfxccatin12lem3  11272  rennim  11521  xrmaxiflemcom  11768  m1expe  12418  m1expo  12419  m1exp1  12420  nn0o1gt2  12424  flodddiv4  12455  cncongr1  12633  m1dvdsndvds  12779  mgmsscl  13402  mndinvmod  13486  ringinvnzdiv  14021  txcn  14957  relogbcxpbap  15647  logbgcd1irr  15649  logbgcd1irraplemexp  15650  fsumdvdsmul  15673  zabsle1  15686  2lgslem1c  15777  2lgsoddprmlem3  15798  upgrpredgv  15952  usgredg2vlem2  16029  ushgredgedg  16032  ushgredgedgloop  16034  ifpsnprss  16064  upgrwlkvtxedg  16085  uspgr2wlkeq  16086  bj-inf2vnlem2  16358