Theorem eqcoms 2180

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-ext 2159

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

This theorem is referenced by:  gencbvex  2783  gencbval  2785  sbceq2a  2973  eqimss2  3210  uneqdifeqim  3508  tppreq3  3695  copsex2t  4243  copsex2g  4244  ordsoexmid  4559  0elsucexmid  4562  ordpwsucexmid  4567  cnveqb  5081  cnveq0  5082  relcoi1  5157  funtpg  5264  f0rn0  5407  f1ocnvfv  5775  f1ocnvfvb  5776  cbvfo  5781  cbvexfo  5782  brabvv  5916  ov6g  6007  ectocld  6596  ecoptocl  6617  phplem3  6849  f1dmvrnfibi  6938  f1vrnfibi  6939  updjud  7076  pr2ne  7186  nn0ind-raph  9364  nn01to3  9611  modqmuladd  10359  modqmuladdnn0  10361  fihashf1rn  10759  hashfzp1  10795  rennim  11002  xrmaxiflemcom  11248  m1expe  11894  m1expo  11895  m1exp1  11896  nn0o1gt2  11900  flodddiv4  11929  cncongr1  12093  m1dvdsndvds  12238  mgmsscl  12710  mndinvmod  12774  ringinvnzdiv  13127  txcn  13557  relogbcxpbap  14165  logbgcd1irr  14167  logbgcd1irraplemexp  14168  zabsle1  14182  bj-inf2vnlem2  14494