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  2784  gencbval  2786  sbceq2a  2974  eqimss2  3211  uneqdifeqim  3509  tppreq3  3696  copsex2t  4246  copsex2g  4247  ordsoexmid  4562  0elsucexmid  4565  ordpwsucexmid  4570  cnveqb  5085  cnveq0  5086  relcoi1  5161  funtpg  5268  f0rn0  5411  f1ocnvfv  5780  f1ocnvfvb  5781  cbvfo  5786  cbvexfo  5787  brabvv  5921  ov6g  6012  ectocld  6601  ecoptocl  6622  phplem3  6854  f1dmvrnfibi  6943  f1vrnfibi  6944  updjud  7081  pr2ne  7191  nn0ind-raph  9370  nn01to3  9617  modqmuladd  10366  modqmuladdnn0  10368  fihashf1rn  10768  hashfzp1  10804  rennim  11011  xrmaxiflemcom  11257  m1expe  11904  m1expo  11905  m1exp1  11906  nn0o1gt2  11910  flodddiv4  11939  cncongr1  12103  m1dvdsndvds  12248  mgmsscl  12780  mndinvmod  12846  ringinvnzdiv  13227  txcn  13778  relogbcxpbap  14386  logbgcd1irr  14388  logbgcd1irraplemexp  14389  zabsle1  14403  2lgsoddprmlem3  14462  bj-inf2vnlem2  14726