Theorem eqcoms 2209

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  gencbvex  2820  gencbval  2822  sbceq2a  3010  eqimss2  3249  uneqdifeqim  3547  tppreq3  3737  copsex2t  4293  copsex2g  4294  ordsoexmid  4614  0elsucexmid  4617  ordpwsucexmid  4622  cnveqb  5143  cnveq0  5144  relcoi1  5219  funtpg  5330  f0rn0  5477  fimadmfo  5514  f1ocnvfv  5855  f1ocnvfvb  5856  cbvfo  5861  cbvexfo  5862  brabvv  5998  ov6g  6091  ectocld  6695  ecoptocl  6716  phplem3  6958  f1dmvrnfibi  7053  f1vrnfibi  7054  updjud  7191  pr2ne  7307  nn0ind-raph  9497  nn01to3  9745  modqmuladd  10518  modqmuladdnn0  10520  fihashf1rn  10940  hashfzp1  10976  lswlgt0cl  11053  rennim  11357  xrmaxiflemcom  11604  m1expe  12254  m1expo  12255  m1exp1  12256  nn0o1gt2  12260  flodddiv4  12291  cncongr1  12469  m1dvdsndvds  12615  mgmsscl  13237  mndinvmod  13321  ringinvnzdiv  13856  txcn  14791  relogbcxpbap  15481  logbgcd1irr  15483  logbgcd1irraplemexp  15484  fsumdvdsmul  15507  zabsle1  15520  2lgslem1c  15611  2lgsoddprmlem3  15632  bj-inf2vnlem2  15981