Theorem eqcoms 2212

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

Syntax hints:   → wi 4   = wceq 1375

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 1473  ax-gen 1475  ax-ext 2191

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

This theorem is referenced by:  gencbvex  2827  gencbval  2829  sbceq2a  3019  eqimss2  3259  uneqdifeqim  3557  tppreq3  3749  copsex2t  4310  copsex2g  4311  ordsoexmid  4631  0elsucexmid  4634  ordpwsucexmid  4639  cnveqb  5160  cnveq0  5161  relcoi1  5236  funtpg  5348  f0rn0  5496  fimadmfo  5533  f1ocnvfv  5876  f1ocnvfvb  5877  cbvfo  5882  cbvexfo  5883  riotaeqimp  5952  brabvv  6021  ov6g  6114  ectocld  6718  ecoptocl  6739  phplem3  6983  f1dmvrnfibi  7079  f1vrnfibi  7080  updjud  7217  pr2ne  7333  nn0ind-raph  9532  nn01to3  9780  modqmuladd  10555  modqmuladdnn0  10557  fihashf1rn  10977  hashfzp1  11013  lswlgt0cl  11090  wrd2ind  11221  pfxccatin12lem2  11229  pfxccatin12lem3  11230  rennim  11479  xrmaxiflemcom  11726  m1expe  12376  m1expo  12377  m1exp1  12378  nn0o1gt2  12382  flodddiv4  12413  cncongr1  12591  m1dvdsndvds  12737  mgmsscl  13360  mndinvmod  13444  ringinvnzdiv  13979  txcn  14914  relogbcxpbap  15604  logbgcd1irr  15606  logbgcd1irraplemexp  15607  fsumdvdsmul  15630  zabsle1  15643  2lgslem1c  15734  2lgsoddprmlem3  15755  upgrpredgv  15909  usgredg2vlem2  15986  ushgredgedg  15989  ushgredgedgloop  15991  bj-inf2vnlem2  16244