Theorem eqcoms 2140

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

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  gencbvex  2727  gencbval  2729  sbceq2a  2914  eqimss2  3147  uneqdifeqim  3443  tppreq3  3621  copsex2t  4162  copsex2g  4163  ordsoexmid  4472  0elsucexmid  4475  ordpwsucexmid  4480  cnveqb  4989  cnveq0  4990  relcoi1  5065  funtpg  5169  f0rn0  5312  f1ocnvfv  5673  f1ocnvfvb  5674  cbvfo  5679  cbvexfo  5680  brabvv  5810  ov6g  5901  ectocld  6488  ecoptocl  6509  phplem3  6741  f1dmvrnfibi  6825  f1vrnfibi  6826  updjud  6960  pr2ne  7041  nn0ind-raph  9161  nn01to3  9402  modqmuladd  10132  modqmuladdnn0  10134  fihashf1rn  10528  hashfzp1  10563  rennim  10767  xrmaxiflemcom  11011  m1expe  11585  m1expo  11586  m1exp1  11587  nn0o1gt2  11591  flodddiv4  11620  cncongr1  11773  txcn  12433  bj-inf2vnlem2  13158